YES 2.1590000000000003 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



HASKELL
  ↳ BR

mainModule Main
  ((lookup :: (Eq c, Eq b) => Either c b  ->  [(Either c b,a)]  ->  Maybe a) :: (Eq b, Eq c) => Either c b  ->  [(Either c b,a)]  ->  Maybe a)

module Main where
  import qualified Prelude



Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ BR
HASKELL
      ↳ COR

mainModule Main
  ((lookup :: (Eq a, Eq b) => Either a b  ->  [(Either a b,c)]  ->  Maybe c) :: (Eq b, Eq a) => Either a b  ->  [(Either a b,c)]  ->  Maybe c)

module Main where
  import qualified Prelude



Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False

The following Function with conditions
lookup k [] = Nothing
lookup k ((x,y: xys)
 | k == x
 = Just y
 | otherwise
 = lookup k xys

is transformed to
lookup k [] = lookup3 k []
lookup k ((x,y: xys) = lookup2 k ((x,y: xys)

lookup0 k x y xys True = lookup k xys

lookup1 k x y xys True = Just y
lookup1 k x y xys False = lookup0 k x y xys otherwise

lookup2 k ((x,y: xys) = lookup1 k x y xys (k == x)

lookup3 k [] = Nothing
lookup3 xy xz = lookup2 xy xz



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
HASKELL
          ↳ Narrow

mainModule Main
  (lookup :: (Eq c, Eq b) => Either c b  ->  [(Either c b,a)]  ->  Maybe a)

module Main where
  import qualified Prelude



Haskell To QDPs


↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(yu4000), Succ(yu40001000)) → new_primPlusNat(yu4000, yu40001000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat(Succ(yu30100), Succ(yu4000100)) → new_primMulNat(yu30100, Succ(yu4000100))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primEqNat(Succ(yu3000), Succ(yu400000)) → new_primEqNat(yu3000, yu400000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_esEs0(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), fa, dh, app(app(ty_@2, hc), hd)) → new_esEs3(yu302, yu40002, hc, hd)
new_esEs0(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), app(app(ty_Either, df), dg), dh, ea) → new_esEs(yu300, yu40000, df, dg)
new_esEs3(@2(yu300, yu301), @2(yu40000, yu40001), bdb, app(ty_Maybe, bea)) → new_esEs2(yu301, yu40001, bea)
new_esEs0(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), app(ty_[], ee), dh, ea) → new_esEs1(yu300, yu40000, ee)
new_esEs0(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), fa, dh, app(ty_Maybe, hb)) → new_esEs2(yu302, yu40002, hb)
new_esEs0(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), app(ty_Maybe, ef), dh, ea) → new_esEs2(yu300, yu40000, ef)
new_esEs2(Just(yu300), Just(yu40000), app(app(ty_Either, bag), bah)) → new_esEs(yu300, yu40000, bag, bah)
new_esEs0(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), fa, dh, app(app(ty_Either, gd), ge)) → new_esEs(yu302, yu40002, gd, ge)
new_esEs0(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), fa, app(ty_[], fh), ea) → new_esEs1(yu301, yu40001, fh)
new_esEs(Right(yu300), Right(yu40000), cc, app(app(app(ty_@3, cf), cg), da)) → new_esEs0(yu300, yu40000, cf, cg, da)
new_esEs(Right(yu300), Right(yu40000), cc, app(ty_[], db)) → new_esEs1(yu300, yu40000, db)
new_esEs1(:(yu300, yu301), :(yu40000, yu40001), baf) → new_esEs1(yu301, yu40001, baf)
new_esEs(Right(yu300), Right(yu40000), cc, app(app(ty_@2, dd), de)) → new_esEs3(yu300, yu40000, dd, de)
new_esEs3(@2(yu300, yu301), @2(yu40000, yu40001), app(app(app(ty_@3, bcc), bcd), bce), bcb) → new_esEs0(yu300, yu40000, bcc, bcd, bce)
new_esEs1(:(yu300, yu301), :(yu40000, yu40001), app(ty_[], bab)) → new_esEs1(yu300, yu40000, bab)
new_esEs3(@2(yu300, yu301), @2(yu40000, yu40001), bdb, app(ty_[], bdh)) → new_esEs1(yu301, yu40001, bdh)
new_esEs2(Just(yu300), Just(yu40000), app(ty_[], bbd)) → new_esEs1(yu300, yu40000, bbd)
new_esEs2(Just(yu300), Just(yu40000), app(ty_Maybe, bbe)) → new_esEs2(yu300, yu40000, bbe)
new_esEs0(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), fa, app(app(app(ty_@3, fd), ff), fg), ea) → new_esEs0(yu301, yu40001, fd, ff, fg)
new_esEs(Left(yu300), Left(yu40000), app(app(app(ty_@3, bd), be), bf), bc) → new_esEs0(yu300, yu40000, bd, be, bf)
new_esEs3(@2(yu300, yu301), @2(yu40000, yu40001), app(ty_[], bcf), bcb) → new_esEs1(yu300, yu40000, bcf)
new_esEs(Left(yu300), Left(yu40000), app(ty_Maybe, bh), bc) → new_esEs2(yu300, yu40000, bh)
new_esEs0(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), fa, app(app(ty_@2, gb), gc), ea) → new_esEs3(yu301, yu40001, gb, gc)
new_esEs0(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), fa, dh, app(ty_[], ha)) → new_esEs1(yu302, yu40002, ha)
new_esEs2(Just(yu300), Just(yu40000), app(app(app(ty_@3, bba), bbb), bbc)) → new_esEs0(yu300, yu40000, bba, bbb, bbc)
new_esEs3(@2(yu300, yu301), @2(yu40000, yu40001), bdb, app(app(ty_@2, beb), bec)) → new_esEs3(yu301, yu40001, beb, bec)
new_esEs0(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), app(app(ty_@2, eg), eh), dh, ea) → new_esEs3(yu300, yu40000, eg, eh)
new_esEs1(:(yu300, yu301), :(yu40000, yu40001), app(app(ty_@2, bad), bae)) → new_esEs3(yu300, yu40000, bad, bae)
new_esEs(Right(yu300), Right(yu40000), cc, app(app(ty_Either, cd), ce)) → new_esEs(yu300, yu40000, cd, ce)
new_esEs(Left(yu300), Left(yu40000), app(app(ty_@2, ca), cb), bc) → new_esEs3(yu300, yu40000, ca, cb)
new_esEs3(@2(yu300, yu301), @2(yu40000, yu40001), app(ty_Maybe, bcg), bcb) → new_esEs2(yu300, yu40000, bcg)
new_esEs0(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), fa, dh, app(app(app(ty_@3, gf), gg), gh)) → new_esEs0(yu302, yu40002, gf, gg, gh)
new_esEs1(:(yu300, yu301), :(yu40000, yu40001), app(ty_Maybe, bac)) → new_esEs2(yu300, yu40000, bac)
new_esEs3(@2(yu300, yu301), @2(yu40000, yu40001), app(app(ty_@2, bch), bda), bcb) → new_esEs3(yu300, yu40000, bch, bda)
new_esEs(Right(yu300), Right(yu40000), cc, app(ty_Maybe, dc)) → new_esEs2(yu300, yu40000, dc)
new_esEs1(:(yu300, yu301), :(yu40000, yu40001), app(app(app(ty_@3, hg), hh), baa)) → new_esEs0(yu300, yu40000, hg, hh, baa)
new_esEs3(@2(yu300, yu301), @2(yu40000, yu40001), bdb, app(app(ty_Either, bdc), bdd)) → new_esEs(yu301, yu40001, bdc, bdd)
new_esEs2(Just(yu300), Just(yu40000), app(app(ty_@2, bbf), bbg)) → new_esEs3(yu300, yu40000, bbf, bbg)
new_esEs3(@2(yu300, yu301), @2(yu40000, yu40001), app(app(ty_Either, bbh), bca), bcb) → new_esEs(yu300, yu40000, bbh, bca)
new_esEs(Left(yu300), Left(yu40000), app(ty_[], bg), bc) → new_esEs1(yu300, yu40000, bg)
new_esEs0(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), fa, app(app(ty_Either, fb), fc), ea) → new_esEs(yu301, yu40001, fb, fc)
new_esEs3(@2(yu300, yu301), @2(yu40000, yu40001), bdb, app(app(app(ty_@3, bde), bdf), bdg)) → new_esEs0(yu301, yu40001, bde, bdf, bdg)
new_esEs0(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), fa, app(ty_Maybe, ga), ea) → new_esEs2(yu301, yu40001, ga)
new_esEs1(:(yu300, yu301), :(yu40000, yu40001), app(app(ty_Either, he), hf)) → new_esEs(yu300, yu40000, he, hf)
new_esEs(Left(yu300), Left(yu40000), app(app(ty_Either, ba), bb), bc) → new_esEs(yu300, yu40000, ba, bb)
new_esEs0(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), app(app(app(ty_@3, eb), ec), ed), dh, ea) → new_esEs0(yu300, yu40000, eb, ec, ed)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
QDP
                ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

new_lookup(Left(yu30), :(@2(Right(yu4000), yu401), yu41), bd, be, bf) → new_lookup(Left(yu30), yu41, bd, be, bf)
new_lookup10(yu22, yu23, yu24, yu25, False, bg, bh, ca) → new_lookup(Right(yu22), yu25, bg, bh, ca)
new_lookup(Right(yu30), :(@2(Right(yu4000), yu401), yu41), bd, be, bf) → new_lookup10(yu30, yu4000, yu401, yu41, new_esEs5(yu30, yu4000, bf), bd, be, bf)
new_lookup1(yu11, yu12, yu13, yu14, False, ba, bb, bc) → new_lookup(Left(yu11), yu14, ba, bb, bc)
new_lookup(Right(yu30), :(@2(Left(yu4000), yu401), yu41), bd, be, bf) → new_lookup(Right(yu30), yu41, bd, be, bf)
new_lookup(Left(yu30), :(@2(Left(yu4000), yu401), yu41), bd, be, bf) → new_lookup1(yu30, yu4000, yu401, yu41, new_esEs4(yu30, yu4000, be), bd, be, bf)

The TRS R consists of the following rules:

new_esEs21(yu301, yu40001, ty_Float) → new_esEs15(yu301, yu40001)
new_esEs22(yu302, yu40002, ty_Bool) → new_esEs18(yu302, yu40002)
new_primPlusNat1(Succ(yu4000), Succ(yu40001000)) → Succ(Succ(new_primPlusNat1(yu4000, yu40001000)))
new_esEs4(yu30, yu4000, ty_@0) → new_esEs16(yu30, yu4000)
new_primEqInt(Neg(Succ(yu3000)), Pos(yu40000)) → False
new_primEqInt(Pos(Succ(yu3000)), Neg(yu40000)) → False
new_esEs5(yu30, yu4000, ty_Int) → new_esEs12(yu30, yu4000)
new_esEs20(yu300, yu40000, ty_@0) → new_esEs16(yu300, yu40000)
new_esEs9(GT, LT) → False
new_esEs9(LT, GT) → False
new_esEs7(Char(yu300), Char(yu40000)) → new_primEqNat0(yu300, yu40000)
new_esEs11(Right(yu300), Right(yu40000), bcf, app(ty_[], bhf)) → new_esEs17(yu300, yu40000, bhf)
new_esEs5(yu30, yu4000, ty_Ordering) → new_esEs9(yu30, yu4000)
new_primEqInt(Neg(Zero), Pos(Succ(yu400000))) → False
new_primEqInt(Pos(Zero), Neg(Succ(yu400000))) → False
new_esEs4(yu30, yu4000, app(app(app(ty_@3, df), dg), dh)) → new_esEs13(yu30, yu4000, df, dg, dh)
new_esEs5(yu30, yu4000, app(ty_Ratio, bbc)) → new_esEs8(yu30, yu4000, bbc)
new_esEs21(yu301, yu40001, app(app(ty_Either, fd), ff)) → new_esEs11(yu301, yu40001, fd, ff)
new_esEs17(:(yu300, yu301), :(yu40000, yu40001), hh) → new_asAs(new_esEs23(yu300, yu40000, hh), new_esEs17(yu301, yu40001, hh))
new_esEs11(Right(yu300), Right(yu40000), bcf, ty_Integer) → new_esEs10(yu300, yu40000)
new_esEs11(Right(yu300), Right(yu40000), bcf, app(ty_Maybe, bhg)) → new_esEs6(yu300, yu40000, bhg)
new_esEs21(yu301, yu40001, app(app(ty_@2, gd), ge)) → new_esEs19(yu301, yu40001, gd, ge)
new_esEs4(yu30, yu4000, app(app(ty_Either, bcf), bcg)) → new_esEs11(yu30, yu4000, bcf, bcg)
new_esEs22(yu302, yu40002, ty_Ordering) → new_esEs9(yu302, yu40002)
new_esEs22(yu302, yu40002, ty_@0) → new_esEs16(yu302, yu40002)
new_esEs23(yu300, yu40000, app(ty_[], bag)) → new_esEs17(yu300, yu40000, bag)
new_esEs25(yu301, yu40001, ty_Float) → new_esEs15(yu301, yu40001)
new_esEs13(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), df, dg, dh) → new_asAs(new_esEs20(yu300, yu40000, df), new_asAs(new_esEs21(yu301, yu40001, dg), new_esEs22(yu302, yu40002, dh)))
new_esEs6(Just(yu300), Just(yu40000), ty_@0) → new_esEs16(yu300, yu40000)
new_esEs21(yu301, yu40001, app(ty_[], gb)) → new_esEs17(yu301, yu40001, gb)
new_primMulNat0(Zero, Zero) → Zero
new_esEs21(yu301, yu40001, ty_Int) → new_esEs12(yu301, yu40001)
new_esEs22(yu302, yu40002, ty_Char) → new_esEs7(yu302, yu40002)
new_esEs4(yu30, yu4000, app(ty_[], hh)) → new_esEs17(yu30, yu4000, hh)
new_esEs22(yu302, yu40002, app(ty_Ratio, gf)) → new_esEs8(yu302, yu40002, gf)
new_esEs27(yu301, yu40001, ty_Integer) → new_esEs10(yu301, yu40001)
new_esEs4(yu30, yu4000, ty_Int) → new_esEs12(yu30, yu4000)
new_esEs4(yu30, yu4000, app(ty_Maybe, cb)) → new_esEs6(yu30, yu4000, cb)
new_primPlusNat0(Zero, yu4000100) → Succ(yu4000100)
new_esEs20(yu300, yu40000, ty_Bool) → new_esEs18(yu300, yu40000)
new_esEs9(GT, GT) → True
new_esEs4(yu30, yu4000, ty_Float) → new_esEs15(yu30, yu4000)
new_esEs6(Just(yu300), Just(yu40000), ty_Ordering) → new_esEs9(yu300, yu40000)
new_esEs20(yu300, yu40000, ty_Integer) → new_esEs10(yu300, yu40000)
new_esEs11(Left(yu300), Left(yu40000), ty_Char, bcg) → new_esEs7(yu300, yu40000)
new_esEs25(yu301, yu40001, ty_Integer) → new_esEs10(yu301, yu40001)
new_esEs5(yu30, yu4000, app(ty_Maybe, bcb)) → new_esEs6(yu30, yu4000, bcb)
new_sr(Pos(yu3010), Neg(yu400010)) → Neg(new_primMulNat0(yu3010, yu400010))
new_sr(Neg(yu3010), Pos(yu400010)) → Neg(new_primMulNat0(yu3010, yu400010))
new_esEs24(yu300, yu40000, app(ty_[], bdh)) → new_esEs17(yu300, yu40000, bdh)
new_esEs6(Just(yu300), Just(yu40000), app(app(ty_Either, cd), ce)) → new_esEs11(yu300, yu40000, cd, ce)
new_esEs6(Just(yu300), Just(yu40000), ty_Float) → new_esEs15(yu300, yu40000)
new_esEs11(Right(yu300), Right(yu40000), bcf, app(app(ty_Either, bha), bhb)) → new_esEs11(yu300, yu40000, bha, bhb)
new_esEs24(yu300, yu40000, ty_Char) → new_esEs7(yu300, yu40000)
new_esEs22(yu302, yu40002, app(ty_Maybe, he)) → new_esEs6(yu302, yu40002, he)
new_esEs24(yu300, yu40000, app(ty_Ratio, bdb)) → new_esEs8(yu300, yu40000, bdb)
new_esEs5(yu30, yu4000, ty_Char) → new_esEs7(yu30, yu4000)
new_esEs20(yu300, yu40000, app(app(ty_Either, eb), ec)) → new_esEs11(yu300, yu40000, eb, ec)
new_esEs23(yu300, yu40000, ty_Integer) → new_esEs10(yu300, yu40000)
new_esEs25(yu301, yu40001, ty_Double) → new_esEs14(yu301, yu40001)
new_esEs23(yu300, yu40000, app(ty_Ratio, baa)) → new_esEs8(yu300, yu40000, baa)
new_esEs11(Right(yu300), Right(yu40000), bcf, ty_Char) → new_esEs7(yu300, yu40000)
new_esEs11(Right(yu300), Right(yu40000), bcf, app(ty_Ratio, bgh)) → new_esEs8(yu300, yu40000, bgh)
new_esEs23(yu300, yu40000, ty_Ordering) → new_esEs9(yu300, yu40000)
new_esEs11(Left(yu300), Left(yu40000), app(app(ty_Either, bfg), bfh), bcg) → new_esEs11(yu300, yu40000, bfg, bfh)
new_esEs22(yu302, yu40002, ty_Integer) → new_esEs10(yu302, yu40002)
new_primEqNat0(Zero, Succ(yu400000)) → False
new_primEqNat0(Succ(yu3000), Zero) → False
new_esEs25(yu301, yu40001, app(ty_Maybe, bfc)) → new_esEs6(yu301, yu40001, bfc)
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_esEs22(yu302, yu40002, ty_Double) → new_esEs14(yu302, yu40002)
new_esEs20(yu300, yu40000, app(app(ty_@2, fa), fb)) → new_esEs19(yu300, yu40000, fa, fb)
new_esEs21(yu301, yu40001, ty_Integer) → new_esEs10(yu301, yu40001)
new_esEs10(Integer(yu300), Integer(yu40000)) → new_primEqInt(yu300, yu40000)
new_esEs25(yu301, yu40001, ty_Int) → new_esEs12(yu301, yu40001)
new_esEs6(Just(yu300), Just(yu40000), app(app(ty_@2, dd), de)) → new_esEs19(yu300, yu40000, dd, de)
new_esEs20(yu300, yu40000, app(ty_[], eg)) → new_esEs17(yu300, yu40000, eg)
new_esEs15(Float(yu300, yu301), Float(yu40000, yu40001)) → new_esEs12(new_sr(yu300, yu40000), new_sr(yu301, yu40001))
new_esEs5(yu30, yu4000, app(app(app(ty_@3, bbf), bbg), bbh)) → new_esEs13(yu30, yu4000, bbf, bbg, bbh)
new_esEs22(yu302, yu40002, app(ty_[], hd)) → new_esEs17(yu302, yu40002, hd)
new_esEs5(yu30, yu4000, ty_Bool) → new_esEs18(yu30, yu4000)
new_esEs11(Right(yu300), Right(yu40000), bcf, app(app(ty_@2, bhh), caa)) → new_esEs19(yu300, yu40000, bhh, caa)
new_esEs4(yu30, yu4000, ty_Double) → new_esEs14(yu30, yu4000)
new_esEs21(yu301, yu40001, app(app(app(ty_@3, fg), fh), ga)) → new_esEs13(yu301, yu40001, fg, fh, ga)
new_esEs23(yu300, yu40000, app(app(ty_Either, bab), bac)) → new_esEs11(yu300, yu40000, bab, bac)
new_esEs6(Just(yu300), Just(yu40000), app(ty_Ratio, cc)) → new_esEs8(yu300, yu40000, cc)
new_esEs12(yu30, yu4000) → new_primEqInt(yu30, yu4000)
new_esEs6(Just(yu300), Just(yu40000), ty_Int) → new_esEs12(yu300, yu40000)
new_esEs9(GT, EQ) → False
new_esEs9(EQ, GT) → False
new_esEs22(yu302, yu40002, app(app(ty_@2, hf), hg)) → new_esEs19(yu302, yu40002, hf, hg)
new_esEs23(yu300, yu40000, ty_Char) → new_esEs7(yu300, yu40000)
new_esEs5(yu30, yu4000, app(app(ty_@2, bcc), bcd)) → new_esEs19(yu30, yu4000, bcc, bcd)
new_esEs5(yu30, yu4000, ty_@0) → new_esEs16(yu30, yu4000)
new_esEs6(Just(yu300), Just(yu40000), app(ty_[], db)) → new_esEs17(yu300, yu40000, db)
new_esEs23(yu300, yu40000, ty_Double) → new_esEs14(yu300, yu40000)
new_esEs6(Just(yu300), Just(yu40000), app(app(app(ty_@3, cf), cg), da)) → new_esEs13(yu300, yu40000, cf, cg, da)
new_esEs22(yu302, yu40002, ty_Float) → new_esEs15(yu302, yu40002)
new_esEs11(Right(yu300), Right(yu40000), bcf, app(app(app(ty_@3, bhc), bhd), bhe)) → new_esEs13(yu300, yu40000, bhc, bhd, bhe)
new_esEs24(yu300, yu40000, ty_Int) → new_esEs12(yu300, yu40000)
new_esEs20(yu300, yu40000, app(ty_Maybe, eh)) → new_esEs6(yu300, yu40000, eh)
new_sr(Neg(yu3010), Neg(yu400010)) → Pos(new_primMulNat0(yu3010, yu400010))
new_esEs21(yu301, yu40001, ty_Bool) → new_esEs18(yu301, yu40001)
new_asAs(False, yu39) → False
new_sr(Pos(yu3010), Pos(yu400010)) → Pos(new_primMulNat0(yu3010, yu400010))
new_esEs23(yu300, yu40000, ty_@0) → new_esEs16(yu300, yu40000)
new_esEs14(Double(yu300, yu301), Double(yu40000, yu40001)) → new_esEs12(new_sr(yu300, yu40000), new_sr(yu301, yu40001))
new_primEqNat0(Zero, Zero) → True
new_esEs6(Just(yu300), Just(yu40000), ty_Bool) → new_esEs18(yu300, yu40000)
new_primMulNat0(Succ(yu30100), Zero) → Zero
new_primMulNat0(Zero, Succ(yu4000100)) → Zero
new_esEs5(yu30, yu4000, app(app(ty_Either, bbd), bbe)) → new_esEs11(yu30, yu4000, bbd, bbe)
new_esEs11(Left(yu300), Left(yu40000), ty_Float, bcg) → new_esEs15(yu300, yu40000)
new_esEs6(Just(yu300), Just(yu40000), app(ty_Maybe, dc)) → new_esEs6(yu300, yu40000, dc)
new_esEs25(yu301, yu40001, ty_@0) → new_esEs16(yu301, yu40001)
new_esEs11(Right(yu300), Right(yu40000), bcf, ty_Ordering) → new_esEs9(yu300, yu40000)
new_esEs25(yu301, yu40001, ty_Bool) → new_esEs18(yu301, yu40001)
new_esEs25(yu301, yu40001, app(ty_Ratio, bed)) → new_esEs8(yu301, yu40001, bed)
new_esEs18(True, True) → True
new_esEs25(yu301, yu40001, ty_Char) → new_esEs7(yu301, yu40001)
new_esEs23(yu300, yu40000, app(app(app(ty_@3, bad), bae), baf)) → new_esEs13(yu300, yu40000, bad, bae, baf)
new_esEs6(Just(yu300), Just(yu40000), ty_Double) → new_esEs14(yu300, yu40000)
new_esEs22(yu302, yu40002, app(app(app(ty_@3, ha), hb), hc)) → new_esEs13(yu302, yu40002, ha, hb, hc)
new_esEs23(yu300, yu40000, ty_Float) → new_esEs15(yu300, yu40000)
new_esEs23(yu300, yu40000, app(ty_Maybe, bah)) → new_esEs6(yu300, yu40000, bah)
new_esEs20(yu300, yu40000, app(ty_Ratio, ea)) → new_esEs8(yu300, yu40000, ea)
new_esEs25(yu301, yu40001, app(ty_[], bfb)) → new_esEs17(yu301, yu40001, bfb)
new_esEs11(Left(yu300), Left(yu40000), ty_Double, bcg) → new_esEs14(yu300, yu40000)
new_esEs26(yu300, yu40000, ty_Int) → new_esEs12(yu300, yu40000)
new_esEs11(Left(yu300), Left(yu40000), app(ty_[], bgd), bcg) → new_esEs17(yu300, yu40000, bgd)
new_esEs16(@0, @0) → True
new_primPlusNat0(Succ(yu400), yu4000100) → Succ(Succ(new_primPlusNat1(yu400, yu4000100)))
new_esEs24(yu300, yu40000, ty_Integer) → new_esEs10(yu300, yu40000)
new_esEs23(yu300, yu40000, ty_Bool) → new_esEs18(yu300, yu40000)
new_esEs11(Right(yu300), Right(yu40000), bcf, ty_Double) → new_esEs14(yu300, yu40000)
new_esEs4(yu30, yu4000, app(ty_Ratio, bce)) → new_esEs8(yu30, yu4000, bce)
new_esEs20(yu300, yu40000, ty_Ordering) → new_esEs9(yu300, yu40000)
new_esEs23(yu300, yu40000, ty_Int) → new_esEs12(yu300, yu40000)
new_esEs21(yu301, yu40001, ty_Ordering) → new_esEs9(yu301, yu40001)
new_esEs25(yu301, yu40001, app(app(app(ty_@3, beg), beh), bfa)) → new_esEs13(yu301, yu40001, beg, beh, bfa)
new_esEs4(yu30, yu4000, ty_Bool) → new_esEs18(yu30, yu4000)
new_esEs4(yu30, yu4000, ty_Integer) → new_esEs10(yu30, yu4000)
new_esEs9(EQ, EQ) → True
new_primEqInt(Neg(Succ(yu3000)), Neg(Succ(yu400000))) → new_primEqNat0(yu3000, yu400000)
new_esEs24(yu300, yu40000, ty_Bool) → new_esEs18(yu300, yu40000)
new_esEs21(yu301, yu40001, app(ty_Ratio, fc)) → new_esEs8(yu301, yu40001, fc)
new_esEs11(Left(yu300), Left(yu40000), ty_Integer, bcg) → new_esEs10(yu300, yu40000)
new_esEs4(yu30, yu4000, ty_Char) → new_esEs7(yu30, yu4000)
new_primPlusNat1(Succ(yu4000), Zero) → Succ(yu4000)
new_primPlusNat1(Zero, Succ(yu40001000)) → Succ(yu40001000)
new_esEs21(yu301, yu40001, ty_@0) → new_esEs16(yu301, yu40001)
new_esEs11(Left(yu300), Left(yu40000), app(app(ty_@2, bgf), bgg), bcg) → new_esEs19(yu300, yu40000, bgf, bgg)
new_esEs11(Right(yu300), Right(yu40000), bcf, ty_Float) → new_esEs15(yu300, yu40000)
new_esEs20(yu300, yu40000, ty_Int) → new_esEs12(yu300, yu40000)
new_esEs11(Left(yu300), Left(yu40000), ty_Bool, bcg) → new_esEs18(yu300, yu40000)
new_esEs9(EQ, LT) → False
new_esEs9(LT, EQ) → False
new_esEs21(yu301, yu40001, ty_Double) → new_esEs14(yu301, yu40001)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_esEs20(yu300, yu40000, ty_Char) → new_esEs7(yu300, yu40000)
new_esEs27(yu301, yu40001, ty_Int) → new_esEs12(yu301, yu40001)
new_esEs5(yu30, yu4000, ty_Integer) → new_esEs10(yu30, yu4000)
new_esEs24(yu300, yu40000, app(app(app(ty_@3, bde), bdf), bdg)) → new_esEs13(yu300, yu40000, bde, bdf, bdg)
new_esEs11(Left(yu300), Left(yu40000), app(ty_Ratio, bff), bcg) → new_esEs8(yu300, yu40000, bff)
new_esEs18(True, False) → False
new_esEs18(False, True) → False
new_primEqInt(Neg(Zero), Neg(Succ(yu400000))) → False
new_primEqInt(Neg(Succ(yu3000)), Neg(Zero)) → False
new_esEs25(yu301, yu40001, ty_Ordering) → new_esEs9(yu301, yu40001)
new_esEs8(:%(yu300, yu301), :%(yu40000, yu40001), bce) → new_asAs(new_esEs26(yu300, yu40000, bce), new_esEs27(yu301, yu40001, bce))
new_esEs19(@2(yu300, yu301), @2(yu40000, yu40001), bch, bda) → new_asAs(new_esEs24(yu300, yu40000, bch), new_esEs25(yu301, yu40001, bda))
new_esEs5(yu30, yu4000, ty_Double) → new_esEs14(yu30, yu4000)
new_esEs20(yu300, yu40000, app(app(app(ty_@3, ed), ee), ef)) → new_esEs13(yu300, yu40000, ed, ee, ef)
new_esEs24(yu300, yu40000, ty_Ordering) → new_esEs9(yu300, yu40000)
new_esEs11(Right(yu300), Right(yu40000), bcf, ty_@0) → new_esEs16(yu300, yu40000)
new_esEs25(yu301, yu40001, app(app(ty_Either, bee), bef)) → new_esEs11(yu301, yu40001, bee, bef)
new_esEs4(yu30, yu4000, app(app(ty_@2, bch), bda)) → new_esEs19(yu30, yu4000, bch, bda)
new_primPlusNat1(Zero, Zero) → Zero
new_esEs22(yu302, yu40002, ty_Int) → new_esEs12(yu302, yu40002)
new_esEs11(Left(yu300), Left(yu40000), app(ty_Maybe, bge), bcg) → new_esEs6(yu300, yu40000, bge)
new_esEs11(Left(yu300), Left(yu40000), ty_@0, bcg) → new_esEs16(yu300, yu40000)
new_asAs(True, yu39) → yu39
new_esEs11(Left(yu300), Left(yu40000), ty_Ordering, bcg) → new_esEs9(yu300, yu40000)
new_primMulNat0(Succ(yu30100), Succ(yu4000100)) → new_primPlusNat0(new_primMulNat0(yu30100, Succ(yu4000100)), yu4000100)
new_esEs6(Nothing, Nothing, cb) → True
new_primEqInt(Pos(Succ(yu3000)), Pos(Succ(yu400000))) → new_primEqNat0(yu3000, yu400000)
new_esEs26(yu300, yu40000, ty_Integer) → new_esEs10(yu300, yu40000)
new_esEs4(yu30, yu4000, ty_Ordering) → new_esEs9(yu30, yu4000)
new_esEs21(yu301, yu40001, app(ty_Maybe, gc)) → new_esEs6(yu301, yu40001, gc)
new_esEs17([], [], hh) → True
new_esEs17(:(yu300, yu301), [], hh) → False
new_esEs17([], :(yu40000, yu40001), hh) → False
new_esEs22(yu302, yu40002, app(app(ty_Either, gg), gh)) → new_esEs11(yu302, yu40002, gg, gh)
new_esEs11(Right(yu300), Right(yu40000), bcf, ty_Bool) → new_esEs18(yu300, yu40000)
new_esEs5(yu30, yu4000, app(ty_[], bca)) → new_esEs17(yu30, yu4000, bca)
new_esEs6(Just(yu300), Nothing, cb) → False
new_esEs6(Nothing, Just(yu40000), cb) → False
new_esEs23(yu300, yu40000, app(app(ty_@2, bba), bbb)) → new_esEs19(yu300, yu40000, bba, bbb)
new_primEqNat0(Succ(yu3000), Succ(yu400000)) → new_primEqNat0(yu3000, yu400000)
new_esEs24(yu300, yu40000, ty_@0) → new_esEs16(yu300, yu40000)
new_esEs24(yu300, yu40000, app(ty_Maybe, bea)) → new_esEs6(yu300, yu40000, bea)
new_esEs11(Left(yu300), Left(yu40000), app(app(app(ty_@3, bga), bgb), bgc), bcg) → new_esEs13(yu300, yu40000, bga, bgb, bgc)
new_esEs25(yu301, yu40001, app(app(ty_@2, bfd), bfe)) → new_esEs19(yu301, yu40001, bfd, bfe)
new_esEs20(yu300, yu40000, ty_Double) → new_esEs14(yu300, yu40000)
new_esEs9(LT, LT) → True
new_esEs11(Right(yu300), Right(yu40000), bcf, ty_Int) → new_esEs12(yu300, yu40000)
new_esEs20(yu300, yu40000, ty_Float) → new_esEs15(yu300, yu40000)
new_esEs21(yu301, yu40001, ty_Char) → new_esEs7(yu301, yu40001)
new_esEs5(yu30, yu4000, ty_Float) → new_esEs15(yu30, yu4000)
new_esEs11(Left(yu300), Left(yu40000), ty_Int, bcg) → new_esEs12(yu300, yu40000)
new_esEs24(yu300, yu40000, app(app(ty_Either, bdc), bdd)) → new_esEs11(yu300, yu40000, bdc, bdd)
new_esEs6(Just(yu300), Just(yu40000), ty_Char) → new_esEs7(yu300, yu40000)
new_primEqInt(Pos(Zero), Pos(Succ(yu400000))) → False
new_primEqInt(Pos(Succ(yu3000)), Pos(Zero)) → False
new_esEs24(yu300, yu40000, app(app(ty_@2, beb), bec)) → new_esEs19(yu300, yu40000, beb, bec)
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_esEs24(yu300, yu40000, ty_Float) → new_esEs15(yu300, yu40000)
new_esEs24(yu300, yu40000, ty_Double) → new_esEs14(yu300, yu40000)
new_esEs6(Just(yu300), Just(yu40000), ty_Integer) → new_esEs10(yu300, yu40000)
new_esEs18(False, False) → True
new_esEs11(Left(yu300), Right(yu40000), bcf, bcg) → False
new_esEs11(Right(yu300), Left(yu40000), bcf, bcg) → False

The set Q consists of the following terms:

new_esEs23(x0, x1, ty_Int)
new_esEs21(x0, x1, ty_Int)
new_esEs9(GT, GT)
new_esEs25(x0, x1, ty_Double)
new_esEs4(x0, x1, ty_Bool)
new_esEs27(x0, x1, ty_Int)
new_esEs4(x0, x1, ty_Integer)
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_esEs22(x0, x1, ty_Ordering)
new_esEs5(x0, x1, ty_Char)
new_primEqInt(Neg(Zero), Pos(Zero))
new_primEqInt(Pos(Zero), Neg(Zero))
new_esEs22(x0, x1, ty_Char)
new_esEs4(x0, x1, ty_Char)
new_esEs5(x0, x1, ty_Float)
new_esEs4(x0, x1, app(app(ty_Either, x2), x3))
new_esEs25(x0, x1, ty_Integer)
new_esEs20(x0, x1, ty_Bool)
new_esEs11(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs11(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs10(Integer(x0), Integer(x1))
new_esEs6(Nothing, Just(x0), x1)
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs18(False, True)
new_esEs18(True, False)
new_esEs4(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs5(x0, x1, ty_Bool)
new_esEs6(Just(x0), Just(x1), ty_Double)
new_esEs9(EQ, EQ)
new_esEs25(x0, x1, ty_Bool)
new_esEs11(Right(x0), Right(x1), x2, ty_Int)
new_esEs24(x0, x1, ty_Ordering)
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs11(Right(x0), Right(x1), x2, ty_Integer)
new_esEs6(Just(x0), Nothing, x1)
new_esEs4(x0, x1, ty_@0)
new_esEs11(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs19(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs22(x0, x1, ty_@0)
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs6(Just(x0), Just(x1), ty_@0)
new_esEs5(x0, x1, app(ty_Maybe, x2))
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs11(Left(x0), Left(x1), ty_Float, x2)
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_esEs11(Right(x0), Right(x1), x2, ty_Char)
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_sr(Neg(x0), Neg(x1))
new_esEs22(x0, x1, ty_Int)
new_esEs17([], :(x0, x1), x2)
new_esEs4(x0, x1, ty_Double)
new_esEs18(True, True)
new_esEs6(Just(x0), Just(x1), ty_Integer)
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_esEs20(x0, x1, ty_Char)
new_esEs7(Char(x0), Char(x1))
new_esEs5(x0, x1, ty_@0)
new_esEs9(LT, GT)
new_esEs9(GT, LT)
new_esEs11(Right(x0), Right(x1), x2, ty_Ordering)
new_primPlusNat0(Zero, x0)
new_esEs25(x0, x1, app(ty_[], x2))
new_esEs24(x0, x1, ty_Bool)
new_esEs16(@0, @0)
new_esEs6(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs21(x0, x1, ty_Ordering)
new_esEs6(Just(x0), Just(x1), ty_Float)
new_esEs23(x0, x1, ty_Ordering)
new_esEs9(GT, EQ)
new_esEs9(EQ, GT)
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_asAs(False, x0)
new_esEs4(x0, x1, ty_Ordering)
new_esEs5(x0, x1, ty_Double)
new_esEs23(x0, x1, ty_Char)
new_esEs20(x0, x1, ty_Integer)
new_esEs6(Just(x0), Just(x1), ty_Bool)
new_esEs17(:(x0, x1), [], x2)
new_esEs5(x0, x1, ty_Ordering)
new_primPlusNat1(Zero, Succ(x0))
new_esEs11(Left(x0), Left(x1), ty_Int, x2)
new_esEs24(x0, x1, ty_Char)
new_esEs4(x0, x1, ty_Float)
new_esEs25(x0, x1, ty_Char)
new_esEs20(x0, x1, app(ty_[], x2))
new_esEs20(x0, x1, ty_Int)
new_esEs5(x0, x1, app(ty_Ratio, x2))
new_esEs26(x0, x1, ty_Int)
new_esEs23(x0, x1, ty_Bool)
new_primEqNat0(Zero, Zero)
new_esEs23(x0, x1, ty_Integer)
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_primMulNat0(Zero, Succ(x0))
new_esEs11(Left(x0), Left(x1), ty_@0, x2)
new_primEqNat0(Succ(x0), Zero)
new_esEs20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs24(x0, x1, ty_Float)
new_esEs6(Just(x0), Just(x1), ty_Int)
new_esEs22(x0, x1, ty_Bool)
new_primPlusNat0(Succ(x0), x1)
new_esEs6(Nothing, Nothing, x0)
new_esEs6(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs11(Right(x0), Right(x1), x2, ty_@0)
new_esEs11(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_esEs21(x0, x1, ty_Float)
new_primMulNat0(Zero, Zero)
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_asAs(True, x0)
new_esEs20(x0, x1, ty_Ordering)
new_esEs5(x0, x1, ty_Integer)
new_esEs21(x0, x1, app(ty_Ratio, x2))
new_esEs21(x0, x1, ty_@0)
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs5(x0, x1, ty_Int)
new_esEs6(Just(x0), Just(x1), ty_Char)
new_esEs11(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs22(x0, x1, app(ty_[], x2))
new_esEs13(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs11(Left(x0), Left(x1), ty_Bool, x2)
new_esEs20(x0, x1, ty_Double)
new_primMulNat0(Succ(x0), Zero)
new_esEs6(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs11(Right(x0), Right(x1), x2, ty_Bool)
new_esEs11(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_sr(Pos(x0), Pos(x1))
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_esEs20(x0, x1, ty_Float)
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs22(x0, x1, ty_Double)
new_esEs11(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs12(x0, x1)
new_esEs5(x0, x1, app(ty_[], x2))
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs11(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs9(LT, EQ)
new_esEs9(EQ, LT)
new_esEs15(Float(x0, x1), Float(x2, x3))
new_esEs11(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs23(x0, x1, ty_Double)
new_esEs6(Just(x0), Just(x1), app(ty_[], x2))
new_esEs25(x0, x1, ty_Int)
new_esEs4(x0, x1, app(ty_[], x2))
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs17(:(x0, x1), :(x2, x3), x4)
new_esEs23(x0, x1, ty_Float)
new_esEs25(x0, x1, ty_Ordering)
new_esEs11(Left(x0), Left(x1), ty_Double, x2)
new_esEs24(x0, x1, app(ty_[], x2))
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs18(False, False)
new_esEs21(x0, x1, ty_Double)
new_esEs20(x0, x1, app(ty_Ratio, x2))
new_esEs4(x0, x1, app(ty_Ratio, x2))
new_esEs24(x0, x1, ty_Int)
new_esEs21(x0, x1, app(ty_[], x2))
new_esEs4(x0, x1, ty_Int)
new_esEs22(x0, x1, ty_Integer)
new_esEs20(x0, x1, ty_@0)
new_esEs23(x0, x1, ty_@0)
new_esEs11(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs20(x0, x1, app(app(ty_Either, x2), x3))
new_esEs11(Left(x0), Left(x1), ty_Integer, x2)
new_primPlusNat1(Succ(x0), Zero)
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs6(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs23(x0, x1, app(ty_[], x2))
new_primMulNat0(Succ(x0), Succ(x1))
new_primPlusNat1(Zero, Zero)
new_esEs24(x0, x1, ty_Double)
new_esEs17([], [], x0)
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs27(x0, x1, ty_Integer)
new_esEs22(x0, x1, ty_Float)
new_esEs26(x0, x1, ty_Integer)
new_esEs24(x0, x1, app(ty_Maybe, x2))
new_esEs4(x0, x1, app(ty_Maybe, x2))
new_esEs5(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs25(x0, x1, ty_@0)
new_esEs5(x0, x1, app(app(ty_Either, x2), x3))
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs11(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs11(Right(x0), Right(x1), x2, ty_Double)
new_esEs4(x0, x1, app(app(ty_@2, x2), x3))
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_esEs6(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs6(Just(x0), Just(x1), ty_Ordering)
new_esEs11(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs21(x0, x1, ty_Char)
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs11(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_esEs25(x0, x1, ty_Float)
new_esEs11(Left(x0), Right(x1), x2, x3)
new_esEs11(Right(x0), Left(x1), x2, x3)
new_esEs24(x0, x1, ty_@0)
new_esEs5(x0, x1, app(app(ty_@2, x2), x3))
new_primEqNat0(Zero, Succ(x0))
new_esEs8(:%(x0, x1), :%(x2, x3), x4)
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_esEs21(x0, x1, ty_Bool)
new_esEs24(x0, x1, ty_Integer)
new_esEs11(Right(x0), Right(x1), x2, ty_Float)
new_esEs11(Left(x0), Left(x1), ty_Char, x2)
new_esEs20(x0, x1, app(ty_Maybe, x2))
new_esEs9(LT, LT)
new_esEs14(Double(x0, x1), Double(x2, x3))
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_sr(Neg(x0), Pos(x1))
new_sr(Pos(x0), Neg(x1))
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_esEs20(x0, x1, app(app(ty_@2, x2), x3))
new_esEs21(x0, x1, ty_Integer)
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs.

↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
                ↳ DependencyGraphProof
                  ↳ AND
QDP
                      ↳ UsableRulesProof
                    ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_lookup10(yu22, yu23, yu24, yu25, False, bg, bh, ca) → new_lookup(Right(yu22), yu25, bg, bh, ca)
new_lookup(Right(yu30), :(@2(Right(yu4000), yu401), yu41), bd, be, bf) → new_lookup10(yu30, yu4000, yu401, yu41, new_esEs5(yu30, yu4000, bf), bd, be, bf)
new_lookup(Right(yu30), :(@2(Left(yu4000), yu401), yu41), bd, be, bf) → new_lookup(Right(yu30), yu41, bd, be, bf)

The TRS R consists of the following rules:

new_esEs21(yu301, yu40001, ty_Float) → new_esEs15(yu301, yu40001)
new_esEs22(yu302, yu40002, ty_Bool) → new_esEs18(yu302, yu40002)
new_primPlusNat1(Succ(yu4000), Succ(yu40001000)) → Succ(Succ(new_primPlusNat1(yu4000, yu40001000)))
new_esEs4(yu30, yu4000, ty_@0) → new_esEs16(yu30, yu4000)
new_primEqInt(Neg(Succ(yu3000)), Pos(yu40000)) → False
new_primEqInt(Pos(Succ(yu3000)), Neg(yu40000)) → False
new_esEs5(yu30, yu4000, ty_Int) → new_esEs12(yu30, yu4000)
new_esEs20(yu300, yu40000, ty_@0) → new_esEs16(yu300, yu40000)
new_esEs9(GT, LT) → False
new_esEs9(LT, GT) → False
new_esEs7(Char(yu300), Char(yu40000)) → new_primEqNat0(yu300, yu40000)
new_esEs11(Right(yu300), Right(yu40000), bcf, app(ty_[], bhf)) → new_esEs17(yu300, yu40000, bhf)
new_esEs5(yu30, yu4000, ty_Ordering) → new_esEs9(yu30, yu4000)
new_primEqInt(Neg(Zero), Pos(Succ(yu400000))) → False
new_primEqInt(Pos(Zero), Neg(Succ(yu400000))) → False
new_esEs4(yu30, yu4000, app(app(app(ty_@3, df), dg), dh)) → new_esEs13(yu30, yu4000, df, dg, dh)
new_esEs5(yu30, yu4000, app(ty_Ratio, bbc)) → new_esEs8(yu30, yu4000, bbc)
new_esEs21(yu301, yu40001, app(app(ty_Either, fd), ff)) → new_esEs11(yu301, yu40001, fd, ff)
new_esEs17(:(yu300, yu301), :(yu40000, yu40001), hh) → new_asAs(new_esEs23(yu300, yu40000, hh), new_esEs17(yu301, yu40001, hh))
new_esEs11(Right(yu300), Right(yu40000), bcf, ty_Integer) → new_esEs10(yu300, yu40000)
new_esEs11(Right(yu300), Right(yu40000), bcf, app(ty_Maybe, bhg)) → new_esEs6(yu300, yu40000, bhg)
new_esEs21(yu301, yu40001, app(app(ty_@2, gd), ge)) → new_esEs19(yu301, yu40001, gd, ge)
new_esEs4(yu30, yu4000, app(app(ty_Either, bcf), bcg)) → new_esEs11(yu30, yu4000, bcf, bcg)
new_esEs22(yu302, yu40002, ty_Ordering) → new_esEs9(yu302, yu40002)
new_esEs22(yu302, yu40002, ty_@0) → new_esEs16(yu302, yu40002)
new_esEs23(yu300, yu40000, app(ty_[], bag)) → new_esEs17(yu300, yu40000, bag)
new_esEs25(yu301, yu40001, ty_Float) → new_esEs15(yu301, yu40001)
new_esEs13(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), df, dg, dh) → new_asAs(new_esEs20(yu300, yu40000, df), new_asAs(new_esEs21(yu301, yu40001, dg), new_esEs22(yu302, yu40002, dh)))
new_esEs6(Just(yu300), Just(yu40000), ty_@0) → new_esEs16(yu300, yu40000)
new_esEs21(yu301, yu40001, app(ty_[], gb)) → new_esEs17(yu301, yu40001, gb)
new_primMulNat0(Zero, Zero) → Zero
new_esEs21(yu301, yu40001, ty_Int) → new_esEs12(yu301, yu40001)
new_esEs22(yu302, yu40002, ty_Char) → new_esEs7(yu302, yu40002)
new_esEs4(yu30, yu4000, app(ty_[], hh)) → new_esEs17(yu30, yu4000, hh)
new_esEs22(yu302, yu40002, app(ty_Ratio, gf)) → new_esEs8(yu302, yu40002, gf)
new_esEs27(yu301, yu40001, ty_Integer) → new_esEs10(yu301, yu40001)
new_esEs4(yu30, yu4000, ty_Int) → new_esEs12(yu30, yu4000)
new_esEs4(yu30, yu4000, app(ty_Maybe, cb)) → new_esEs6(yu30, yu4000, cb)
new_primPlusNat0(Zero, yu4000100) → Succ(yu4000100)
new_esEs20(yu300, yu40000, ty_Bool) → new_esEs18(yu300, yu40000)
new_esEs9(GT, GT) → True
new_esEs4(yu30, yu4000, ty_Float) → new_esEs15(yu30, yu4000)
new_esEs6(Just(yu300), Just(yu40000), ty_Ordering) → new_esEs9(yu300, yu40000)
new_esEs20(yu300, yu40000, ty_Integer) → new_esEs10(yu300, yu40000)
new_esEs11(Left(yu300), Left(yu40000), ty_Char, bcg) → new_esEs7(yu300, yu40000)
new_esEs25(yu301, yu40001, ty_Integer) → new_esEs10(yu301, yu40001)
new_esEs5(yu30, yu4000, app(ty_Maybe, bcb)) → new_esEs6(yu30, yu4000, bcb)
new_sr(Pos(yu3010), Neg(yu400010)) → Neg(new_primMulNat0(yu3010, yu400010))
new_sr(Neg(yu3010), Pos(yu400010)) → Neg(new_primMulNat0(yu3010, yu400010))
new_esEs24(yu300, yu40000, app(ty_[], bdh)) → new_esEs17(yu300, yu40000, bdh)
new_esEs6(Just(yu300), Just(yu40000), app(app(ty_Either, cd), ce)) → new_esEs11(yu300, yu40000, cd, ce)
new_esEs6(Just(yu300), Just(yu40000), ty_Float) → new_esEs15(yu300, yu40000)
new_esEs11(Right(yu300), Right(yu40000), bcf, app(app(ty_Either, bha), bhb)) → new_esEs11(yu300, yu40000, bha, bhb)
new_esEs24(yu300, yu40000, ty_Char) → new_esEs7(yu300, yu40000)
new_esEs22(yu302, yu40002, app(ty_Maybe, he)) → new_esEs6(yu302, yu40002, he)
new_esEs24(yu300, yu40000, app(ty_Ratio, bdb)) → new_esEs8(yu300, yu40000, bdb)
new_esEs5(yu30, yu4000, ty_Char) → new_esEs7(yu30, yu4000)
new_esEs20(yu300, yu40000, app(app(ty_Either, eb), ec)) → new_esEs11(yu300, yu40000, eb, ec)
new_esEs23(yu300, yu40000, ty_Integer) → new_esEs10(yu300, yu40000)
new_esEs25(yu301, yu40001, ty_Double) → new_esEs14(yu301, yu40001)
new_esEs23(yu300, yu40000, app(ty_Ratio, baa)) → new_esEs8(yu300, yu40000, baa)
new_esEs11(Right(yu300), Right(yu40000), bcf, ty_Char) → new_esEs7(yu300, yu40000)
new_esEs11(Right(yu300), Right(yu40000), bcf, app(ty_Ratio, bgh)) → new_esEs8(yu300, yu40000, bgh)
new_esEs23(yu300, yu40000, ty_Ordering) → new_esEs9(yu300, yu40000)
new_esEs11(Left(yu300), Left(yu40000), app(app(ty_Either, bfg), bfh), bcg) → new_esEs11(yu300, yu40000, bfg, bfh)
new_esEs22(yu302, yu40002, ty_Integer) → new_esEs10(yu302, yu40002)
new_primEqNat0(Zero, Succ(yu400000)) → False
new_primEqNat0(Succ(yu3000), Zero) → False
new_esEs25(yu301, yu40001, app(ty_Maybe, bfc)) → new_esEs6(yu301, yu40001, bfc)
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_esEs22(yu302, yu40002, ty_Double) → new_esEs14(yu302, yu40002)
new_esEs20(yu300, yu40000, app(app(ty_@2, fa), fb)) → new_esEs19(yu300, yu40000, fa, fb)
new_esEs21(yu301, yu40001, ty_Integer) → new_esEs10(yu301, yu40001)
new_esEs10(Integer(yu300), Integer(yu40000)) → new_primEqInt(yu300, yu40000)
new_esEs25(yu301, yu40001, ty_Int) → new_esEs12(yu301, yu40001)
new_esEs6(Just(yu300), Just(yu40000), app(app(ty_@2, dd), de)) → new_esEs19(yu300, yu40000, dd, de)
new_esEs20(yu300, yu40000, app(ty_[], eg)) → new_esEs17(yu300, yu40000, eg)
new_esEs15(Float(yu300, yu301), Float(yu40000, yu40001)) → new_esEs12(new_sr(yu300, yu40000), new_sr(yu301, yu40001))
new_esEs5(yu30, yu4000, app(app(app(ty_@3, bbf), bbg), bbh)) → new_esEs13(yu30, yu4000, bbf, bbg, bbh)
new_esEs22(yu302, yu40002, app(ty_[], hd)) → new_esEs17(yu302, yu40002, hd)
new_esEs5(yu30, yu4000, ty_Bool) → new_esEs18(yu30, yu4000)
new_esEs11(Right(yu300), Right(yu40000), bcf, app(app(ty_@2, bhh), caa)) → new_esEs19(yu300, yu40000, bhh, caa)
new_esEs4(yu30, yu4000, ty_Double) → new_esEs14(yu30, yu4000)
new_esEs21(yu301, yu40001, app(app(app(ty_@3, fg), fh), ga)) → new_esEs13(yu301, yu40001, fg, fh, ga)
new_esEs23(yu300, yu40000, app(app(ty_Either, bab), bac)) → new_esEs11(yu300, yu40000, bab, bac)
new_esEs6(Just(yu300), Just(yu40000), app(ty_Ratio, cc)) → new_esEs8(yu300, yu40000, cc)
new_esEs12(yu30, yu4000) → new_primEqInt(yu30, yu4000)
new_esEs6(Just(yu300), Just(yu40000), ty_Int) → new_esEs12(yu300, yu40000)
new_esEs9(GT, EQ) → False
new_esEs9(EQ, GT) → False
new_esEs22(yu302, yu40002, app(app(ty_@2, hf), hg)) → new_esEs19(yu302, yu40002, hf, hg)
new_esEs23(yu300, yu40000, ty_Char) → new_esEs7(yu300, yu40000)
new_esEs5(yu30, yu4000, app(app(ty_@2, bcc), bcd)) → new_esEs19(yu30, yu4000, bcc, bcd)
new_esEs5(yu30, yu4000, ty_@0) → new_esEs16(yu30, yu4000)
new_esEs6(Just(yu300), Just(yu40000), app(ty_[], db)) → new_esEs17(yu300, yu40000, db)
new_esEs23(yu300, yu40000, ty_Double) → new_esEs14(yu300, yu40000)
new_esEs6(Just(yu300), Just(yu40000), app(app(app(ty_@3, cf), cg), da)) → new_esEs13(yu300, yu40000, cf, cg, da)
new_esEs22(yu302, yu40002, ty_Float) → new_esEs15(yu302, yu40002)
new_esEs11(Right(yu300), Right(yu40000), bcf, app(app(app(ty_@3, bhc), bhd), bhe)) → new_esEs13(yu300, yu40000, bhc, bhd, bhe)
new_esEs24(yu300, yu40000, ty_Int) → new_esEs12(yu300, yu40000)
new_esEs20(yu300, yu40000, app(ty_Maybe, eh)) → new_esEs6(yu300, yu40000, eh)
new_sr(Neg(yu3010), Neg(yu400010)) → Pos(new_primMulNat0(yu3010, yu400010))
new_esEs21(yu301, yu40001, ty_Bool) → new_esEs18(yu301, yu40001)
new_asAs(False, yu39) → False
new_sr(Pos(yu3010), Pos(yu400010)) → Pos(new_primMulNat0(yu3010, yu400010))
new_esEs23(yu300, yu40000, ty_@0) → new_esEs16(yu300, yu40000)
new_esEs14(Double(yu300, yu301), Double(yu40000, yu40001)) → new_esEs12(new_sr(yu300, yu40000), new_sr(yu301, yu40001))
new_primEqNat0(Zero, Zero) → True
new_esEs6(Just(yu300), Just(yu40000), ty_Bool) → new_esEs18(yu300, yu40000)
new_primMulNat0(Succ(yu30100), Zero) → Zero
new_primMulNat0(Zero, Succ(yu4000100)) → Zero
new_esEs5(yu30, yu4000, app(app(ty_Either, bbd), bbe)) → new_esEs11(yu30, yu4000, bbd, bbe)
new_esEs11(Left(yu300), Left(yu40000), ty_Float, bcg) → new_esEs15(yu300, yu40000)
new_esEs6(Just(yu300), Just(yu40000), app(ty_Maybe, dc)) → new_esEs6(yu300, yu40000, dc)
new_esEs25(yu301, yu40001, ty_@0) → new_esEs16(yu301, yu40001)
new_esEs11(Right(yu300), Right(yu40000), bcf, ty_Ordering) → new_esEs9(yu300, yu40000)
new_esEs25(yu301, yu40001, ty_Bool) → new_esEs18(yu301, yu40001)
new_esEs25(yu301, yu40001, app(ty_Ratio, bed)) → new_esEs8(yu301, yu40001, bed)
new_esEs18(True, True) → True
new_esEs25(yu301, yu40001, ty_Char) → new_esEs7(yu301, yu40001)
new_esEs23(yu300, yu40000, app(app(app(ty_@3, bad), bae), baf)) → new_esEs13(yu300, yu40000, bad, bae, baf)
new_esEs6(Just(yu300), Just(yu40000), ty_Double) → new_esEs14(yu300, yu40000)
new_esEs22(yu302, yu40002, app(app(app(ty_@3, ha), hb), hc)) → new_esEs13(yu302, yu40002, ha, hb, hc)
new_esEs23(yu300, yu40000, ty_Float) → new_esEs15(yu300, yu40000)
new_esEs23(yu300, yu40000, app(ty_Maybe, bah)) → new_esEs6(yu300, yu40000, bah)
new_esEs20(yu300, yu40000, app(ty_Ratio, ea)) → new_esEs8(yu300, yu40000, ea)
new_esEs25(yu301, yu40001, app(ty_[], bfb)) → new_esEs17(yu301, yu40001, bfb)
new_esEs11(Left(yu300), Left(yu40000), ty_Double, bcg) → new_esEs14(yu300, yu40000)
new_esEs26(yu300, yu40000, ty_Int) → new_esEs12(yu300, yu40000)
new_esEs11(Left(yu300), Left(yu40000), app(ty_[], bgd), bcg) → new_esEs17(yu300, yu40000, bgd)
new_esEs16(@0, @0) → True
new_primPlusNat0(Succ(yu400), yu4000100) → Succ(Succ(new_primPlusNat1(yu400, yu4000100)))
new_esEs24(yu300, yu40000, ty_Integer) → new_esEs10(yu300, yu40000)
new_esEs23(yu300, yu40000, ty_Bool) → new_esEs18(yu300, yu40000)
new_esEs11(Right(yu300), Right(yu40000), bcf, ty_Double) → new_esEs14(yu300, yu40000)
new_esEs4(yu30, yu4000, app(ty_Ratio, bce)) → new_esEs8(yu30, yu4000, bce)
new_esEs20(yu300, yu40000, ty_Ordering) → new_esEs9(yu300, yu40000)
new_esEs23(yu300, yu40000, ty_Int) → new_esEs12(yu300, yu40000)
new_esEs21(yu301, yu40001, ty_Ordering) → new_esEs9(yu301, yu40001)
new_esEs25(yu301, yu40001, app(app(app(ty_@3, beg), beh), bfa)) → new_esEs13(yu301, yu40001, beg, beh, bfa)
new_esEs4(yu30, yu4000, ty_Bool) → new_esEs18(yu30, yu4000)
new_esEs4(yu30, yu4000, ty_Integer) → new_esEs10(yu30, yu4000)
new_esEs9(EQ, EQ) → True
new_primEqInt(Neg(Succ(yu3000)), Neg(Succ(yu400000))) → new_primEqNat0(yu3000, yu400000)
new_esEs24(yu300, yu40000, ty_Bool) → new_esEs18(yu300, yu40000)
new_esEs21(yu301, yu40001, app(ty_Ratio, fc)) → new_esEs8(yu301, yu40001, fc)
new_esEs11(Left(yu300), Left(yu40000), ty_Integer, bcg) → new_esEs10(yu300, yu40000)
new_esEs4(yu30, yu4000, ty_Char) → new_esEs7(yu30, yu4000)
new_primPlusNat1(Succ(yu4000), Zero) → Succ(yu4000)
new_primPlusNat1(Zero, Succ(yu40001000)) → Succ(yu40001000)
new_esEs21(yu301, yu40001, ty_@0) → new_esEs16(yu301, yu40001)
new_esEs11(Left(yu300), Left(yu40000), app(app(ty_@2, bgf), bgg), bcg) → new_esEs19(yu300, yu40000, bgf, bgg)
new_esEs11(Right(yu300), Right(yu40000), bcf, ty_Float) → new_esEs15(yu300, yu40000)
new_esEs20(yu300, yu40000, ty_Int) → new_esEs12(yu300, yu40000)
new_esEs11(Left(yu300), Left(yu40000), ty_Bool, bcg) → new_esEs18(yu300, yu40000)
new_esEs9(EQ, LT) → False
new_esEs9(LT, EQ) → False
new_esEs21(yu301, yu40001, ty_Double) → new_esEs14(yu301, yu40001)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_esEs20(yu300, yu40000, ty_Char) → new_esEs7(yu300, yu40000)
new_esEs27(yu301, yu40001, ty_Int) → new_esEs12(yu301, yu40001)
new_esEs5(yu30, yu4000, ty_Integer) → new_esEs10(yu30, yu4000)
new_esEs24(yu300, yu40000, app(app(app(ty_@3, bde), bdf), bdg)) → new_esEs13(yu300, yu40000, bde, bdf, bdg)
new_esEs11(Left(yu300), Left(yu40000), app(ty_Ratio, bff), bcg) → new_esEs8(yu300, yu40000, bff)
new_esEs18(True, False) → False
new_esEs18(False, True) → False
new_primEqInt(Neg(Zero), Neg(Succ(yu400000))) → False
new_primEqInt(Neg(Succ(yu3000)), Neg(Zero)) → False
new_esEs25(yu301, yu40001, ty_Ordering) → new_esEs9(yu301, yu40001)
new_esEs8(:%(yu300, yu301), :%(yu40000, yu40001), bce) → new_asAs(new_esEs26(yu300, yu40000, bce), new_esEs27(yu301, yu40001, bce))
new_esEs19(@2(yu300, yu301), @2(yu40000, yu40001), bch, bda) → new_asAs(new_esEs24(yu300, yu40000, bch), new_esEs25(yu301, yu40001, bda))
new_esEs5(yu30, yu4000, ty_Double) → new_esEs14(yu30, yu4000)
new_esEs20(yu300, yu40000, app(app(app(ty_@3, ed), ee), ef)) → new_esEs13(yu300, yu40000, ed, ee, ef)
new_esEs24(yu300, yu40000, ty_Ordering) → new_esEs9(yu300, yu40000)
new_esEs11(Right(yu300), Right(yu40000), bcf, ty_@0) → new_esEs16(yu300, yu40000)
new_esEs25(yu301, yu40001, app(app(ty_Either, bee), bef)) → new_esEs11(yu301, yu40001, bee, bef)
new_esEs4(yu30, yu4000, app(app(ty_@2, bch), bda)) → new_esEs19(yu30, yu4000, bch, bda)
new_primPlusNat1(Zero, Zero) → Zero
new_esEs22(yu302, yu40002, ty_Int) → new_esEs12(yu302, yu40002)
new_esEs11(Left(yu300), Left(yu40000), app(ty_Maybe, bge), bcg) → new_esEs6(yu300, yu40000, bge)
new_esEs11(Left(yu300), Left(yu40000), ty_@0, bcg) → new_esEs16(yu300, yu40000)
new_asAs(True, yu39) → yu39
new_esEs11(Left(yu300), Left(yu40000), ty_Ordering, bcg) → new_esEs9(yu300, yu40000)
new_primMulNat0(Succ(yu30100), Succ(yu4000100)) → new_primPlusNat0(new_primMulNat0(yu30100, Succ(yu4000100)), yu4000100)
new_esEs6(Nothing, Nothing, cb) → True
new_primEqInt(Pos(Succ(yu3000)), Pos(Succ(yu400000))) → new_primEqNat0(yu3000, yu400000)
new_esEs26(yu300, yu40000, ty_Integer) → new_esEs10(yu300, yu40000)
new_esEs4(yu30, yu4000, ty_Ordering) → new_esEs9(yu30, yu4000)
new_esEs21(yu301, yu40001, app(ty_Maybe, gc)) → new_esEs6(yu301, yu40001, gc)
new_esEs17([], [], hh) → True
new_esEs17(:(yu300, yu301), [], hh) → False
new_esEs17([], :(yu40000, yu40001), hh) → False
new_esEs22(yu302, yu40002, app(app(ty_Either, gg), gh)) → new_esEs11(yu302, yu40002, gg, gh)
new_esEs11(Right(yu300), Right(yu40000), bcf, ty_Bool) → new_esEs18(yu300, yu40000)
new_esEs5(yu30, yu4000, app(ty_[], bca)) → new_esEs17(yu30, yu4000, bca)
new_esEs6(Just(yu300), Nothing, cb) → False
new_esEs6(Nothing, Just(yu40000), cb) → False
new_esEs23(yu300, yu40000, app(app(ty_@2, bba), bbb)) → new_esEs19(yu300, yu40000, bba, bbb)
new_primEqNat0(Succ(yu3000), Succ(yu400000)) → new_primEqNat0(yu3000, yu400000)
new_esEs24(yu300, yu40000, ty_@0) → new_esEs16(yu300, yu40000)
new_esEs24(yu300, yu40000, app(ty_Maybe, bea)) → new_esEs6(yu300, yu40000, bea)
new_esEs11(Left(yu300), Left(yu40000), app(app(app(ty_@3, bga), bgb), bgc), bcg) → new_esEs13(yu300, yu40000, bga, bgb, bgc)
new_esEs25(yu301, yu40001, app(app(ty_@2, bfd), bfe)) → new_esEs19(yu301, yu40001, bfd, bfe)
new_esEs20(yu300, yu40000, ty_Double) → new_esEs14(yu300, yu40000)
new_esEs9(LT, LT) → True
new_esEs11(Right(yu300), Right(yu40000), bcf, ty_Int) → new_esEs12(yu300, yu40000)
new_esEs20(yu300, yu40000, ty_Float) → new_esEs15(yu300, yu40000)
new_esEs21(yu301, yu40001, ty_Char) → new_esEs7(yu301, yu40001)
new_esEs5(yu30, yu4000, ty_Float) → new_esEs15(yu30, yu4000)
new_esEs11(Left(yu300), Left(yu40000), ty_Int, bcg) → new_esEs12(yu300, yu40000)
new_esEs24(yu300, yu40000, app(app(ty_Either, bdc), bdd)) → new_esEs11(yu300, yu40000, bdc, bdd)
new_esEs6(Just(yu300), Just(yu40000), ty_Char) → new_esEs7(yu300, yu40000)
new_primEqInt(Pos(Zero), Pos(Succ(yu400000))) → False
new_primEqInt(Pos(Succ(yu3000)), Pos(Zero)) → False
new_esEs24(yu300, yu40000, app(app(ty_@2, beb), bec)) → new_esEs19(yu300, yu40000, beb, bec)
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_esEs24(yu300, yu40000, ty_Float) → new_esEs15(yu300, yu40000)
new_esEs24(yu300, yu40000, ty_Double) → new_esEs14(yu300, yu40000)
new_esEs6(Just(yu300), Just(yu40000), ty_Integer) → new_esEs10(yu300, yu40000)
new_esEs18(False, False) → True
new_esEs11(Left(yu300), Right(yu40000), bcf, bcg) → False
new_esEs11(Right(yu300), Left(yu40000), bcf, bcg) → False

The set Q consists of the following terms:

new_esEs23(x0, x1, ty_Int)
new_esEs21(x0, x1, ty_Int)
new_esEs9(GT, GT)
new_esEs25(x0, x1, ty_Double)
new_esEs4(x0, x1, ty_Bool)
new_esEs27(x0, x1, ty_Int)
new_esEs4(x0, x1, ty_Integer)
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_esEs22(x0, x1, ty_Ordering)
new_esEs5(x0, x1, ty_Char)
new_primEqInt(Neg(Zero), Pos(Zero))
new_primEqInt(Pos(Zero), Neg(Zero))
new_esEs22(x0, x1, ty_Char)
new_esEs4(x0, x1, ty_Char)
new_esEs5(x0, x1, ty_Float)
new_esEs4(x0, x1, app(app(ty_Either, x2), x3))
new_esEs25(x0, x1, ty_Integer)
new_esEs20(x0, x1, ty_Bool)
new_esEs11(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs11(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs10(Integer(x0), Integer(x1))
new_esEs6(Nothing, Just(x0), x1)
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs18(False, True)
new_esEs18(True, False)
new_esEs4(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs5(x0, x1, ty_Bool)
new_esEs6(Just(x0), Just(x1), ty_Double)
new_esEs9(EQ, EQ)
new_esEs25(x0, x1, ty_Bool)
new_esEs11(Right(x0), Right(x1), x2, ty_Int)
new_esEs24(x0, x1, ty_Ordering)
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs11(Right(x0), Right(x1), x2, ty_Integer)
new_esEs6(Just(x0), Nothing, x1)
new_esEs4(x0, x1, ty_@0)
new_esEs11(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs19(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs22(x0, x1, ty_@0)
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs6(Just(x0), Just(x1), ty_@0)
new_esEs5(x0, x1, app(ty_Maybe, x2))
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs11(Left(x0), Left(x1), ty_Float, x2)
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_esEs11(Right(x0), Right(x1), x2, ty_Char)
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_sr(Neg(x0), Neg(x1))
new_esEs22(x0, x1, ty_Int)
new_esEs17([], :(x0, x1), x2)
new_esEs4(x0, x1, ty_Double)
new_esEs18(True, True)
new_esEs6(Just(x0), Just(x1), ty_Integer)
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_esEs20(x0, x1, ty_Char)
new_esEs7(Char(x0), Char(x1))
new_esEs5(x0, x1, ty_@0)
new_esEs9(LT, GT)
new_esEs9(GT, LT)
new_esEs11(Right(x0), Right(x1), x2, ty_Ordering)
new_primPlusNat0(Zero, x0)
new_esEs25(x0, x1, app(ty_[], x2))
new_esEs24(x0, x1, ty_Bool)
new_esEs16(@0, @0)
new_esEs6(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs21(x0, x1, ty_Ordering)
new_esEs6(Just(x0), Just(x1), ty_Float)
new_esEs23(x0, x1, ty_Ordering)
new_esEs9(GT, EQ)
new_esEs9(EQ, GT)
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_asAs(False, x0)
new_esEs4(x0, x1, ty_Ordering)
new_esEs5(x0, x1, ty_Double)
new_esEs23(x0, x1, ty_Char)
new_esEs20(x0, x1, ty_Integer)
new_esEs6(Just(x0), Just(x1), ty_Bool)
new_esEs17(:(x0, x1), [], x2)
new_esEs5(x0, x1, ty_Ordering)
new_primPlusNat1(Zero, Succ(x0))
new_esEs11(Left(x0), Left(x1), ty_Int, x2)
new_esEs24(x0, x1, ty_Char)
new_esEs4(x0, x1, ty_Float)
new_esEs25(x0, x1, ty_Char)
new_esEs20(x0, x1, app(ty_[], x2))
new_esEs20(x0, x1, ty_Int)
new_esEs5(x0, x1, app(ty_Ratio, x2))
new_esEs26(x0, x1, ty_Int)
new_esEs23(x0, x1, ty_Bool)
new_primEqNat0(Zero, Zero)
new_esEs23(x0, x1, ty_Integer)
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_primMulNat0(Zero, Succ(x0))
new_esEs11(Left(x0), Left(x1), ty_@0, x2)
new_primEqNat0(Succ(x0), Zero)
new_esEs20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs24(x0, x1, ty_Float)
new_esEs6(Just(x0), Just(x1), ty_Int)
new_esEs22(x0, x1, ty_Bool)
new_primPlusNat0(Succ(x0), x1)
new_esEs6(Nothing, Nothing, x0)
new_esEs6(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs11(Right(x0), Right(x1), x2, ty_@0)
new_esEs11(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_esEs21(x0, x1, ty_Float)
new_primMulNat0(Zero, Zero)
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_asAs(True, x0)
new_esEs20(x0, x1, ty_Ordering)
new_esEs5(x0, x1, ty_Integer)
new_esEs21(x0, x1, app(ty_Ratio, x2))
new_esEs21(x0, x1, ty_@0)
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs5(x0, x1, ty_Int)
new_esEs6(Just(x0), Just(x1), ty_Char)
new_esEs11(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs22(x0, x1, app(ty_[], x2))
new_esEs13(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs11(Left(x0), Left(x1), ty_Bool, x2)
new_esEs20(x0, x1, ty_Double)
new_primMulNat0(Succ(x0), Zero)
new_esEs6(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs11(Right(x0), Right(x1), x2, ty_Bool)
new_esEs11(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_sr(Pos(x0), Pos(x1))
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_esEs20(x0, x1, ty_Float)
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs22(x0, x1, ty_Double)
new_esEs11(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs12(x0, x1)
new_esEs5(x0, x1, app(ty_[], x2))
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs11(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs9(LT, EQ)
new_esEs9(EQ, LT)
new_esEs15(Float(x0, x1), Float(x2, x3))
new_esEs11(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs23(x0, x1, ty_Double)
new_esEs6(Just(x0), Just(x1), app(ty_[], x2))
new_esEs25(x0, x1, ty_Int)
new_esEs4(x0, x1, app(ty_[], x2))
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs17(:(x0, x1), :(x2, x3), x4)
new_esEs23(x0, x1, ty_Float)
new_esEs25(x0, x1, ty_Ordering)
new_esEs11(Left(x0), Left(x1), ty_Double, x2)
new_esEs24(x0, x1, app(ty_[], x2))
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs18(False, False)
new_esEs21(x0, x1, ty_Double)
new_esEs20(x0, x1, app(ty_Ratio, x2))
new_esEs4(x0, x1, app(ty_Ratio, x2))
new_esEs24(x0, x1, ty_Int)
new_esEs21(x0, x1, app(ty_[], x2))
new_esEs4(x0, x1, ty_Int)
new_esEs22(x0, x1, ty_Integer)
new_esEs20(x0, x1, ty_@0)
new_esEs23(x0, x1, ty_@0)
new_esEs11(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs20(x0, x1, app(app(ty_Either, x2), x3))
new_esEs11(Left(x0), Left(x1), ty_Integer, x2)
new_primPlusNat1(Succ(x0), Zero)
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs6(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs23(x0, x1, app(ty_[], x2))
new_primMulNat0(Succ(x0), Succ(x1))
new_primPlusNat1(Zero, Zero)
new_esEs24(x0, x1, ty_Double)
new_esEs17([], [], x0)
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs27(x0, x1, ty_Integer)
new_esEs22(x0, x1, ty_Float)
new_esEs26(x0, x1, ty_Integer)
new_esEs24(x0, x1, app(ty_Maybe, x2))
new_esEs4(x0, x1, app(ty_Maybe, x2))
new_esEs5(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs25(x0, x1, ty_@0)
new_esEs5(x0, x1, app(app(ty_Either, x2), x3))
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs11(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs11(Right(x0), Right(x1), x2, ty_Double)
new_esEs4(x0, x1, app(app(ty_@2, x2), x3))
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_esEs6(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs6(Just(x0), Just(x1), ty_Ordering)
new_esEs11(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs21(x0, x1, ty_Char)
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs11(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_esEs25(x0, x1, ty_Float)
new_esEs11(Left(x0), Right(x1), x2, x3)
new_esEs11(Right(x0), Left(x1), x2, x3)
new_esEs24(x0, x1, ty_@0)
new_esEs5(x0, x1, app(app(ty_@2, x2), x3))
new_primEqNat0(Zero, Succ(x0))
new_esEs8(:%(x0, x1), :%(x2, x3), x4)
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_esEs21(x0, x1, ty_Bool)
new_esEs24(x0, x1, ty_Integer)
new_esEs11(Right(x0), Right(x1), x2, ty_Float)
new_esEs11(Left(x0), Left(x1), ty_Char, x2)
new_esEs20(x0, x1, app(ty_Maybe, x2))
new_esEs9(LT, LT)
new_esEs14(Double(x0, x1), Double(x2, x3))
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_sr(Neg(x0), Pos(x1))
new_sr(Pos(x0), Neg(x1))
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_esEs20(x0, x1, app(app(ty_@2, x2), x3))
new_esEs21(x0, x1, ty_Integer)
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
                ↳ DependencyGraphProof
                  ↳ AND
                    ↳ QDP
                      ↳ UsableRulesProof
QDP
                          ↳ QReductionProof
                    ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_lookup10(yu22, yu23, yu24, yu25, False, bg, bh, ca) → new_lookup(Right(yu22), yu25, bg, bh, ca)
new_lookup(Right(yu30), :(@2(Right(yu4000), yu401), yu41), bd, be, bf) → new_lookup10(yu30, yu4000, yu401, yu41, new_esEs5(yu30, yu4000, bf), bd, be, bf)
new_lookup(Right(yu30), :(@2(Left(yu4000), yu401), yu41), bd, be, bf) → new_lookup(Right(yu30), yu41, bd, be, bf)

The TRS R consists of the following rules:

new_esEs5(yu30, yu4000, ty_Int) → new_esEs12(yu30, yu4000)
new_esEs5(yu30, yu4000, ty_Ordering) → new_esEs9(yu30, yu4000)
new_esEs5(yu30, yu4000, app(ty_Ratio, bbc)) → new_esEs8(yu30, yu4000, bbc)
new_esEs5(yu30, yu4000, app(ty_Maybe, bcb)) → new_esEs6(yu30, yu4000, bcb)
new_esEs5(yu30, yu4000, ty_Char) → new_esEs7(yu30, yu4000)
new_esEs5(yu30, yu4000, app(app(app(ty_@3, bbf), bbg), bbh)) → new_esEs13(yu30, yu4000, bbf, bbg, bbh)
new_esEs5(yu30, yu4000, ty_Bool) → new_esEs18(yu30, yu4000)
new_esEs5(yu30, yu4000, app(app(ty_@2, bcc), bcd)) → new_esEs19(yu30, yu4000, bcc, bcd)
new_esEs5(yu30, yu4000, ty_@0) → new_esEs16(yu30, yu4000)
new_esEs5(yu30, yu4000, app(app(ty_Either, bbd), bbe)) → new_esEs11(yu30, yu4000, bbd, bbe)
new_esEs5(yu30, yu4000, ty_Integer) → new_esEs10(yu30, yu4000)
new_esEs5(yu30, yu4000, ty_Double) → new_esEs14(yu30, yu4000)
new_esEs5(yu30, yu4000, app(ty_[], bca)) → new_esEs17(yu30, yu4000, bca)
new_esEs5(yu30, yu4000, ty_Float) → new_esEs15(yu30, yu4000)
new_esEs15(Float(yu300, yu301), Float(yu40000, yu40001)) → new_esEs12(new_sr(yu300, yu40000), new_sr(yu301, yu40001))
new_sr(Pos(yu3010), Neg(yu400010)) → Neg(new_primMulNat0(yu3010, yu400010))
new_sr(Neg(yu3010), Pos(yu400010)) → Neg(new_primMulNat0(yu3010, yu400010))
new_sr(Neg(yu3010), Neg(yu400010)) → Pos(new_primMulNat0(yu3010, yu400010))
new_sr(Pos(yu3010), Pos(yu400010)) → Pos(new_primMulNat0(yu3010, yu400010))
new_esEs12(yu30, yu4000) → new_primEqInt(yu30, yu4000)
new_primEqInt(Neg(Succ(yu3000)), Pos(yu40000)) → False
new_primEqInt(Pos(Succ(yu3000)), Neg(yu40000)) → False
new_primEqInt(Neg(Zero), Pos(Succ(yu400000))) → False
new_primEqInt(Pos(Zero), Neg(Succ(yu400000))) → False
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_primEqInt(Neg(Succ(yu3000)), Neg(Succ(yu400000))) → new_primEqNat0(yu3000, yu400000)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_primEqInt(Neg(Zero), Neg(Succ(yu400000))) → False
new_primEqInt(Neg(Succ(yu3000)), Neg(Zero)) → False
new_primEqInt(Pos(Succ(yu3000)), Pos(Succ(yu400000))) → new_primEqNat0(yu3000, yu400000)
new_primEqInt(Pos(Zero), Pos(Succ(yu400000))) → False
new_primEqInt(Pos(Succ(yu3000)), Pos(Zero)) → False
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_primEqNat0(Zero, Succ(yu400000)) → False
new_primEqNat0(Succ(yu3000), Zero) → False
new_primEqNat0(Zero, Zero) → True
new_primEqNat0(Succ(yu3000), Succ(yu400000)) → new_primEqNat0(yu3000, yu400000)
new_primMulNat0(Zero, Zero) → Zero
new_primMulNat0(Succ(yu30100), Zero) → Zero
new_primMulNat0(Zero, Succ(yu4000100)) → Zero
new_primMulNat0(Succ(yu30100), Succ(yu4000100)) → new_primPlusNat0(new_primMulNat0(yu30100, Succ(yu4000100)), yu4000100)
new_primPlusNat0(Zero, yu4000100) → Succ(yu4000100)
new_primPlusNat0(Succ(yu400), yu4000100) → Succ(Succ(new_primPlusNat1(yu400, yu4000100)))
new_primPlusNat1(Succ(yu4000), Succ(yu40001000)) → Succ(Succ(new_primPlusNat1(yu4000, yu40001000)))
new_primPlusNat1(Succ(yu4000), Zero) → Succ(yu4000)
new_primPlusNat1(Zero, Succ(yu40001000)) → Succ(yu40001000)
new_primPlusNat1(Zero, Zero) → Zero
new_esEs17(:(yu300, yu301), :(yu40000, yu40001), hh) → new_asAs(new_esEs23(yu300, yu40000, hh), new_esEs17(yu301, yu40001, hh))
new_esEs17([], [], hh) → True
new_esEs17(:(yu300, yu301), [], hh) → False
new_esEs17([], :(yu40000, yu40001), hh) → False
new_esEs23(yu300, yu40000, app(ty_[], bag)) → new_esEs17(yu300, yu40000, bag)
new_esEs23(yu300, yu40000, ty_Integer) → new_esEs10(yu300, yu40000)
new_esEs23(yu300, yu40000, app(ty_Ratio, baa)) → new_esEs8(yu300, yu40000, baa)
new_esEs23(yu300, yu40000, ty_Ordering) → new_esEs9(yu300, yu40000)
new_esEs23(yu300, yu40000, app(app(ty_Either, bab), bac)) → new_esEs11(yu300, yu40000, bab, bac)
new_esEs23(yu300, yu40000, ty_Char) → new_esEs7(yu300, yu40000)
new_esEs23(yu300, yu40000, ty_Double) → new_esEs14(yu300, yu40000)
new_esEs23(yu300, yu40000, ty_@0) → new_esEs16(yu300, yu40000)
new_esEs23(yu300, yu40000, app(app(app(ty_@3, bad), bae), baf)) → new_esEs13(yu300, yu40000, bad, bae, baf)
new_esEs23(yu300, yu40000, ty_Float) → new_esEs15(yu300, yu40000)
new_esEs23(yu300, yu40000, app(ty_Maybe, bah)) → new_esEs6(yu300, yu40000, bah)
new_esEs23(yu300, yu40000, ty_Bool) → new_esEs18(yu300, yu40000)
new_esEs23(yu300, yu40000, ty_Int) → new_esEs12(yu300, yu40000)
new_esEs23(yu300, yu40000, app(app(ty_@2, bba), bbb)) → new_esEs19(yu300, yu40000, bba, bbb)
new_asAs(False, yu39) → False
new_asAs(True, yu39) → yu39
new_esEs19(@2(yu300, yu301), @2(yu40000, yu40001), bch, bda) → new_asAs(new_esEs24(yu300, yu40000, bch), new_esEs25(yu301, yu40001, bda))
new_esEs24(yu300, yu40000, app(ty_[], bdh)) → new_esEs17(yu300, yu40000, bdh)
new_esEs24(yu300, yu40000, ty_Char) → new_esEs7(yu300, yu40000)
new_esEs24(yu300, yu40000, app(ty_Ratio, bdb)) → new_esEs8(yu300, yu40000, bdb)
new_esEs24(yu300, yu40000, ty_Int) → new_esEs12(yu300, yu40000)
new_esEs24(yu300, yu40000, ty_Integer) → new_esEs10(yu300, yu40000)
new_esEs24(yu300, yu40000, ty_Bool) → new_esEs18(yu300, yu40000)
new_esEs24(yu300, yu40000, app(app(app(ty_@3, bde), bdf), bdg)) → new_esEs13(yu300, yu40000, bde, bdf, bdg)
new_esEs24(yu300, yu40000, ty_Ordering) → new_esEs9(yu300, yu40000)
new_esEs24(yu300, yu40000, ty_@0) → new_esEs16(yu300, yu40000)
new_esEs24(yu300, yu40000, app(ty_Maybe, bea)) → new_esEs6(yu300, yu40000, bea)
new_esEs24(yu300, yu40000, app(app(ty_Either, bdc), bdd)) → new_esEs11(yu300, yu40000, bdc, bdd)
new_esEs24(yu300, yu40000, app(app(ty_@2, beb), bec)) → new_esEs19(yu300, yu40000, beb, bec)
new_esEs24(yu300, yu40000, ty_Float) → new_esEs15(yu300, yu40000)
new_esEs24(yu300, yu40000, ty_Double) → new_esEs14(yu300, yu40000)
new_esEs25(yu301, yu40001, ty_Float) → new_esEs15(yu301, yu40001)
new_esEs25(yu301, yu40001, ty_Integer) → new_esEs10(yu301, yu40001)
new_esEs25(yu301, yu40001, ty_Double) → new_esEs14(yu301, yu40001)
new_esEs25(yu301, yu40001, app(ty_Maybe, bfc)) → new_esEs6(yu301, yu40001, bfc)
new_esEs25(yu301, yu40001, ty_Int) → new_esEs12(yu301, yu40001)
new_esEs25(yu301, yu40001, ty_@0) → new_esEs16(yu301, yu40001)
new_esEs25(yu301, yu40001, ty_Bool) → new_esEs18(yu301, yu40001)
new_esEs25(yu301, yu40001, app(ty_Ratio, bed)) → new_esEs8(yu301, yu40001, bed)
new_esEs25(yu301, yu40001, ty_Char) → new_esEs7(yu301, yu40001)
new_esEs25(yu301, yu40001, app(ty_[], bfb)) → new_esEs17(yu301, yu40001, bfb)
new_esEs25(yu301, yu40001, app(app(app(ty_@3, beg), beh), bfa)) → new_esEs13(yu301, yu40001, beg, beh, bfa)
new_esEs25(yu301, yu40001, ty_Ordering) → new_esEs9(yu301, yu40001)
new_esEs25(yu301, yu40001, app(app(ty_Either, bee), bef)) → new_esEs11(yu301, yu40001, bee, bef)
new_esEs25(yu301, yu40001, app(app(ty_@2, bfd), bfe)) → new_esEs19(yu301, yu40001, bfd, bfe)
new_esEs11(Right(yu300), Right(yu40000), bcf, app(ty_[], bhf)) → new_esEs17(yu300, yu40000, bhf)
new_esEs11(Right(yu300), Right(yu40000), bcf, ty_Integer) → new_esEs10(yu300, yu40000)
new_esEs6(Just(yu300), Just(yu40000), app(ty_Maybe, dc)) → new_esEs6(yu300, yu40000, dc)
new_esEs11(Left(yu300), Left(yu40000), app(app(ty_Either, bfg), bfh), bcg) → new_esEs11(yu300, yu40000, bfg, bfh)
new_esEs11(Right(yu300), Right(yu40000), bcf, app(app(ty_Either, bha), bhb)) → new_esEs11(yu300, yu40000, bha, bhb)
new_esEs11(Right(yu300), Right(yu40000), bcf, app(ty_Maybe, bhg)) → new_esEs6(yu300, yu40000, bhg)
new_esEs11(Left(yu300), Left(yu40000), app(ty_Maybe, bge), bcg) → new_esEs6(yu300, yu40000, bge)
new_esEs6(Just(yu300), Just(yu40000), app(app(ty_Either, cd), ce)) → new_esEs11(yu300, yu40000, cd, ce)
new_esEs11(Left(yu300), Left(yu40000), ty_Char, bcg) → new_esEs7(yu300, yu40000)
new_esEs11(Right(yu300), Right(yu40000), bcf, ty_Char) → new_esEs7(yu300, yu40000)
new_esEs11(Right(yu300), Right(yu40000), bcf, app(ty_Ratio, bgh)) → new_esEs8(yu300, yu40000, bgh)
new_esEs11(Right(yu300), Right(yu40000), bcf, app(app(ty_@2, bhh), caa)) → new_esEs19(yu300, yu40000, bhh, caa)
new_esEs11(Right(yu300), Right(yu40000), bcf, app(app(app(ty_@3, bhc), bhd), bhe)) → new_esEs13(yu300, yu40000, bhc, bhd, bhe)
new_esEs11(Left(yu300), Left(yu40000), ty_Float, bcg) → new_esEs15(yu300, yu40000)
new_esEs11(Right(yu300), Right(yu40000), bcf, ty_Ordering) → new_esEs9(yu300, yu40000)
new_esEs11(Left(yu300), Left(yu40000), ty_Double, bcg) → new_esEs14(yu300, yu40000)
new_esEs11(Left(yu300), Left(yu40000), app(ty_[], bgd), bcg) → new_esEs17(yu300, yu40000, bgd)
new_esEs11(Right(yu300), Right(yu40000), bcf, ty_Double) → new_esEs14(yu300, yu40000)
new_esEs11(Left(yu300), Left(yu40000), ty_Integer, bcg) → new_esEs10(yu300, yu40000)
new_esEs11(Left(yu300), Left(yu40000), app(app(ty_@2, bgf), bgg), bcg) → new_esEs19(yu300, yu40000, bgf, bgg)
new_esEs11(Right(yu300), Right(yu40000), bcf, ty_Float) → new_esEs15(yu300, yu40000)
new_esEs11(Left(yu300), Left(yu40000), ty_Bool, bcg) → new_esEs18(yu300, yu40000)
new_esEs11(Left(yu300), Left(yu40000), app(ty_Ratio, bff), bcg) → new_esEs8(yu300, yu40000, bff)
new_esEs11(Right(yu300), Right(yu40000), bcf, ty_@0) → new_esEs16(yu300, yu40000)
new_esEs11(Left(yu300), Left(yu40000), ty_@0, bcg) → new_esEs16(yu300, yu40000)
new_esEs11(Left(yu300), Left(yu40000), ty_Ordering, bcg) → new_esEs9(yu300, yu40000)
new_esEs11(Right(yu300), Right(yu40000), bcf, ty_Bool) → new_esEs18(yu300, yu40000)
new_esEs11(Left(yu300), Left(yu40000), app(app(app(ty_@3, bga), bgb), bgc), bcg) → new_esEs13(yu300, yu40000, bga, bgb, bgc)
new_esEs11(Right(yu300), Right(yu40000), bcf, ty_Int) → new_esEs12(yu300, yu40000)
new_esEs11(Left(yu300), Left(yu40000), ty_Int, bcg) → new_esEs12(yu300, yu40000)
new_esEs11(Left(yu300), Right(yu40000), bcf, bcg) → False
new_esEs11(Right(yu300), Left(yu40000), bcf, bcg) → False
new_esEs13(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), df, dg, dh) → new_asAs(new_esEs20(yu300, yu40000, df), new_asAs(new_esEs21(yu301, yu40001, dg), new_esEs22(yu302, yu40002, dh)))
new_esEs20(yu300, yu40000, ty_@0) → new_esEs16(yu300, yu40000)
new_esEs20(yu300, yu40000, ty_Bool) → new_esEs18(yu300, yu40000)
new_esEs20(yu300, yu40000, ty_Integer) → new_esEs10(yu300, yu40000)
new_esEs20(yu300, yu40000, app(app(ty_Either, eb), ec)) → new_esEs11(yu300, yu40000, eb, ec)
new_esEs20(yu300, yu40000, app(app(ty_@2, fa), fb)) → new_esEs19(yu300, yu40000, fa, fb)
new_esEs20(yu300, yu40000, app(ty_[], eg)) → new_esEs17(yu300, yu40000, eg)
new_esEs20(yu300, yu40000, app(ty_Maybe, eh)) → new_esEs6(yu300, yu40000, eh)
new_esEs20(yu300, yu40000, app(ty_Ratio, ea)) → new_esEs8(yu300, yu40000, ea)
new_esEs20(yu300, yu40000, ty_Ordering) → new_esEs9(yu300, yu40000)
new_esEs20(yu300, yu40000, ty_Int) → new_esEs12(yu300, yu40000)
new_esEs20(yu300, yu40000, ty_Char) → new_esEs7(yu300, yu40000)
new_esEs20(yu300, yu40000, app(app(app(ty_@3, ed), ee), ef)) → new_esEs13(yu300, yu40000, ed, ee, ef)
new_esEs20(yu300, yu40000, ty_Double) → new_esEs14(yu300, yu40000)
new_esEs20(yu300, yu40000, ty_Float) → new_esEs15(yu300, yu40000)
new_esEs21(yu301, yu40001, ty_Float) → new_esEs15(yu301, yu40001)
new_esEs21(yu301, yu40001, app(app(ty_Either, fd), ff)) → new_esEs11(yu301, yu40001, fd, ff)
new_esEs21(yu301, yu40001, app(app(ty_@2, gd), ge)) → new_esEs19(yu301, yu40001, gd, ge)
new_esEs21(yu301, yu40001, app(ty_[], gb)) → new_esEs17(yu301, yu40001, gb)
new_esEs21(yu301, yu40001, ty_Int) → new_esEs12(yu301, yu40001)
new_esEs21(yu301, yu40001, ty_Integer) → new_esEs10(yu301, yu40001)
new_esEs21(yu301, yu40001, app(app(app(ty_@3, fg), fh), ga)) → new_esEs13(yu301, yu40001, fg, fh, ga)
new_esEs21(yu301, yu40001, ty_Bool) → new_esEs18(yu301, yu40001)
new_esEs21(yu301, yu40001, ty_Ordering) → new_esEs9(yu301, yu40001)
new_esEs21(yu301, yu40001, app(ty_Ratio, fc)) → new_esEs8(yu301, yu40001, fc)
new_esEs21(yu301, yu40001, ty_@0) → new_esEs16(yu301, yu40001)
new_esEs21(yu301, yu40001, ty_Double) → new_esEs14(yu301, yu40001)
new_esEs21(yu301, yu40001, app(ty_Maybe, gc)) → new_esEs6(yu301, yu40001, gc)
new_esEs21(yu301, yu40001, ty_Char) → new_esEs7(yu301, yu40001)
new_esEs22(yu302, yu40002, ty_Bool) → new_esEs18(yu302, yu40002)
new_esEs22(yu302, yu40002, ty_Ordering) → new_esEs9(yu302, yu40002)
new_esEs22(yu302, yu40002, ty_@0) → new_esEs16(yu302, yu40002)
new_esEs22(yu302, yu40002, ty_Char) → new_esEs7(yu302, yu40002)
new_esEs22(yu302, yu40002, app(ty_Ratio, gf)) → new_esEs8(yu302, yu40002, gf)
new_esEs22(yu302, yu40002, app(ty_Maybe, he)) → new_esEs6(yu302, yu40002, he)
new_esEs22(yu302, yu40002, ty_Integer) → new_esEs10(yu302, yu40002)
new_esEs22(yu302, yu40002, ty_Double) → new_esEs14(yu302, yu40002)
new_esEs22(yu302, yu40002, app(ty_[], hd)) → new_esEs17(yu302, yu40002, hd)
new_esEs22(yu302, yu40002, app(app(ty_@2, hf), hg)) → new_esEs19(yu302, yu40002, hf, hg)
new_esEs22(yu302, yu40002, ty_Float) → new_esEs15(yu302, yu40002)
new_esEs22(yu302, yu40002, app(app(app(ty_@3, ha), hb), hc)) → new_esEs13(yu302, yu40002, ha, hb, hc)
new_esEs22(yu302, yu40002, ty_Int) → new_esEs12(yu302, yu40002)
new_esEs22(yu302, yu40002, app(app(ty_Either, gg), gh)) → new_esEs11(yu302, yu40002, gg, gh)
new_esEs14(Double(yu300, yu301), Double(yu40000, yu40001)) → new_esEs12(new_sr(yu300, yu40000), new_sr(yu301, yu40001))
new_esEs10(Integer(yu300), Integer(yu40000)) → new_primEqInt(yu300, yu40000)
new_esEs6(Just(yu300), Just(yu40000), ty_@0) → new_esEs16(yu300, yu40000)
new_esEs6(Just(yu300), Just(yu40000), ty_Ordering) → new_esEs9(yu300, yu40000)
new_esEs6(Just(yu300), Just(yu40000), ty_Float) → new_esEs15(yu300, yu40000)
new_esEs6(Just(yu300), Just(yu40000), app(app(ty_@2, dd), de)) → new_esEs19(yu300, yu40000, dd, de)
new_esEs6(Just(yu300), Just(yu40000), app(ty_Ratio, cc)) → new_esEs8(yu300, yu40000, cc)
new_esEs6(Just(yu300), Just(yu40000), ty_Int) → new_esEs12(yu300, yu40000)
new_esEs6(Just(yu300), Just(yu40000), app(ty_[], db)) → new_esEs17(yu300, yu40000, db)
new_esEs6(Just(yu300), Just(yu40000), app(app(app(ty_@3, cf), cg), da)) → new_esEs13(yu300, yu40000, cf, cg, da)
new_esEs6(Just(yu300), Just(yu40000), ty_Bool) → new_esEs18(yu300, yu40000)
new_esEs6(Just(yu300), Just(yu40000), ty_Double) → new_esEs14(yu300, yu40000)
new_esEs6(Nothing, Nothing, cb) → True
new_esEs6(Just(yu300), Nothing, cb) → False
new_esEs6(Nothing, Just(yu40000), cb) → False
new_esEs6(Just(yu300), Just(yu40000), ty_Char) → new_esEs7(yu300, yu40000)
new_esEs6(Just(yu300), Just(yu40000), ty_Integer) → new_esEs10(yu300, yu40000)
new_esEs7(Char(yu300), Char(yu40000)) → new_primEqNat0(yu300, yu40000)
new_esEs18(True, True) → True
new_esEs18(True, False) → False
new_esEs18(False, True) → False
new_esEs18(False, False) → True
new_esEs8(:%(yu300, yu301), :%(yu40000, yu40001), bce) → new_asAs(new_esEs26(yu300, yu40000, bce), new_esEs27(yu301, yu40001, bce))
new_esEs26(yu300, yu40000, ty_Int) → new_esEs12(yu300, yu40000)
new_esEs26(yu300, yu40000, ty_Integer) → new_esEs10(yu300, yu40000)
new_esEs27(yu301, yu40001, ty_Integer) → new_esEs10(yu301, yu40001)
new_esEs27(yu301, yu40001, ty_Int) → new_esEs12(yu301, yu40001)
new_esEs9(GT, LT) → False
new_esEs9(LT, GT) → False
new_esEs9(GT, GT) → True
new_esEs9(GT, EQ) → False
new_esEs9(EQ, GT) → False
new_esEs9(EQ, EQ) → True
new_esEs9(EQ, LT) → False
new_esEs9(LT, EQ) → False
new_esEs9(LT, LT) → True
new_esEs16(@0, @0) → True

The set Q consists of the following terms:

new_esEs23(x0, x1, ty_Int)
new_esEs21(x0, x1, ty_Int)
new_esEs9(GT, GT)
new_esEs25(x0, x1, ty_Double)
new_esEs4(x0, x1, ty_Bool)
new_esEs27(x0, x1, ty_Int)
new_esEs4(x0, x1, ty_Integer)
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_esEs22(x0, x1, ty_Ordering)
new_esEs5(x0, x1, ty_Char)
new_primEqInt(Neg(Zero), Pos(Zero))
new_primEqInt(Pos(Zero), Neg(Zero))
new_esEs22(x0, x1, ty_Char)
new_esEs4(x0, x1, ty_Char)
new_esEs5(x0, x1, ty_Float)
new_esEs4(x0, x1, app(app(ty_Either, x2), x3))
new_esEs25(x0, x1, ty_Integer)
new_esEs20(x0, x1, ty_Bool)
new_esEs11(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs11(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs10(Integer(x0), Integer(x1))
new_esEs6(Nothing, Just(x0), x1)
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs18(False, True)
new_esEs18(True, False)
new_esEs4(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs5(x0, x1, ty_Bool)
new_esEs6(Just(x0), Just(x1), ty_Double)
new_esEs9(EQ, EQ)
new_esEs25(x0, x1, ty_Bool)
new_esEs11(Right(x0), Right(x1), x2, ty_Int)
new_esEs24(x0, x1, ty_Ordering)
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs11(Right(x0), Right(x1), x2, ty_Integer)
new_esEs6(Just(x0), Nothing, x1)
new_esEs4(x0, x1, ty_@0)
new_esEs11(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs19(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs22(x0, x1, ty_@0)
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs6(Just(x0), Just(x1), ty_@0)
new_esEs5(x0, x1, app(ty_Maybe, x2))
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs11(Left(x0), Left(x1), ty_Float, x2)
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_esEs11(Right(x0), Right(x1), x2, ty_Char)
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_sr(Neg(x0), Neg(x1))
new_esEs22(x0, x1, ty_Int)
new_esEs17([], :(x0, x1), x2)
new_esEs4(x0, x1, ty_Double)
new_esEs18(True, True)
new_esEs6(Just(x0), Just(x1), ty_Integer)
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_esEs20(x0, x1, ty_Char)
new_esEs7(Char(x0), Char(x1))
new_esEs5(x0, x1, ty_@0)
new_esEs9(LT, GT)
new_esEs9(GT, LT)
new_esEs11(Right(x0), Right(x1), x2, ty_Ordering)
new_primPlusNat0(Zero, x0)
new_esEs25(x0, x1, app(ty_[], x2))
new_esEs24(x0, x1, ty_Bool)
new_esEs16(@0, @0)
new_esEs6(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs21(x0, x1, ty_Ordering)
new_esEs6(Just(x0), Just(x1), ty_Float)
new_esEs23(x0, x1, ty_Ordering)
new_esEs9(GT, EQ)
new_esEs9(EQ, GT)
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_asAs(False, x0)
new_esEs4(x0, x1, ty_Ordering)
new_esEs5(x0, x1, ty_Double)
new_esEs23(x0, x1, ty_Char)
new_esEs20(x0, x1, ty_Integer)
new_esEs6(Just(x0), Just(x1), ty_Bool)
new_esEs17(:(x0, x1), [], x2)
new_esEs5(x0, x1, ty_Ordering)
new_primPlusNat1(Zero, Succ(x0))
new_esEs11(Left(x0), Left(x1), ty_Int, x2)
new_esEs24(x0, x1, ty_Char)
new_esEs4(x0, x1, ty_Float)
new_esEs25(x0, x1, ty_Char)
new_esEs20(x0, x1, app(ty_[], x2))
new_esEs20(x0, x1, ty_Int)
new_esEs5(x0, x1, app(ty_Ratio, x2))
new_esEs26(x0, x1, ty_Int)
new_esEs23(x0, x1, ty_Bool)
new_primEqNat0(Zero, Zero)
new_esEs23(x0, x1, ty_Integer)
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_primMulNat0(Zero, Succ(x0))
new_esEs11(Left(x0), Left(x1), ty_@0, x2)
new_primEqNat0(Succ(x0), Zero)
new_esEs20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs24(x0, x1, ty_Float)
new_esEs6(Just(x0), Just(x1), ty_Int)
new_esEs22(x0, x1, ty_Bool)
new_primPlusNat0(Succ(x0), x1)
new_esEs6(Nothing, Nothing, x0)
new_esEs6(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs11(Right(x0), Right(x1), x2, ty_@0)
new_esEs11(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_esEs21(x0, x1, ty_Float)
new_primMulNat0(Zero, Zero)
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_asAs(True, x0)
new_esEs20(x0, x1, ty_Ordering)
new_esEs5(x0, x1, ty_Integer)
new_esEs21(x0, x1, app(ty_Ratio, x2))
new_esEs21(x0, x1, ty_@0)
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs5(x0, x1, ty_Int)
new_esEs6(Just(x0), Just(x1), ty_Char)
new_esEs11(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs22(x0, x1, app(ty_[], x2))
new_esEs13(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs11(Left(x0), Left(x1), ty_Bool, x2)
new_esEs20(x0, x1, ty_Double)
new_primMulNat0(Succ(x0), Zero)
new_esEs6(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs11(Right(x0), Right(x1), x2, ty_Bool)
new_esEs11(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_sr(Pos(x0), Pos(x1))
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_esEs20(x0, x1, ty_Float)
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs22(x0, x1, ty_Double)
new_esEs11(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs12(x0, x1)
new_esEs5(x0, x1, app(ty_[], x2))
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs11(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs9(LT, EQ)
new_esEs9(EQ, LT)
new_esEs15(Float(x0, x1), Float(x2, x3))
new_esEs11(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs23(x0, x1, ty_Double)
new_esEs6(Just(x0), Just(x1), app(ty_[], x2))
new_esEs25(x0, x1, ty_Int)
new_esEs4(x0, x1, app(ty_[], x2))
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs17(:(x0, x1), :(x2, x3), x4)
new_esEs23(x0, x1, ty_Float)
new_esEs25(x0, x1, ty_Ordering)
new_esEs11(Left(x0), Left(x1), ty_Double, x2)
new_esEs24(x0, x1, app(ty_[], x2))
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs18(False, False)
new_esEs21(x0, x1, ty_Double)
new_esEs20(x0, x1, app(ty_Ratio, x2))
new_esEs4(x0, x1, app(ty_Ratio, x2))
new_esEs24(x0, x1, ty_Int)
new_esEs21(x0, x1, app(ty_[], x2))
new_esEs4(x0, x1, ty_Int)
new_esEs22(x0, x1, ty_Integer)
new_esEs20(x0, x1, ty_@0)
new_esEs23(x0, x1, ty_@0)
new_esEs11(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs20(x0, x1, app(app(ty_Either, x2), x3))
new_esEs11(Left(x0), Left(x1), ty_Integer, x2)
new_primPlusNat1(Succ(x0), Zero)
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs6(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs23(x0, x1, app(ty_[], x2))
new_primMulNat0(Succ(x0), Succ(x1))
new_primPlusNat1(Zero, Zero)
new_esEs24(x0, x1, ty_Double)
new_esEs17([], [], x0)
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs27(x0, x1, ty_Integer)
new_esEs22(x0, x1, ty_Float)
new_esEs26(x0, x1, ty_Integer)
new_esEs24(x0, x1, app(ty_Maybe, x2))
new_esEs4(x0, x1, app(ty_Maybe, x2))
new_esEs5(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs25(x0, x1, ty_@0)
new_esEs5(x0, x1, app(app(ty_Either, x2), x3))
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs11(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs11(Right(x0), Right(x1), x2, ty_Double)
new_esEs4(x0, x1, app(app(ty_@2, x2), x3))
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_esEs6(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs6(Just(x0), Just(x1), ty_Ordering)
new_esEs11(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs21(x0, x1, ty_Char)
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs11(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_esEs25(x0, x1, ty_Float)
new_esEs11(Left(x0), Right(x1), x2, x3)
new_esEs11(Right(x0), Left(x1), x2, x3)
new_esEs24(x0, x1, ty_@0)
new_esEs5(x0, x1, app(app(ty_@2, x2), x3))
new_primEqNat0(Zero, Succ(x0))
new_esEs8(:%(x0, x1), :%(x2, x3), x4)
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_esEs21(x0, x1, ty_Bool)
new_esEs24(x0, x1, ty_Integer)
new_esEs11(Right(x0), Right(x1), x2, ty_Float)
new_esEs11(Left(x0), Left(x1), ty_Char, x2)
new_esEs20(x0, x1, app(ty_Maybe, x2))
new_esEs9(LT, LT)
new_esEs14(Double(x0, x1), Double(x2, x3))
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_sr(Neg(x0), Pos(x1))
new_sr(Pos(x0), Neg(x1))
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_esEs20(x0, x1, app(app(ty_@2, x2), x3))
new_esEs21(x0, x1, ty_Integer)
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_esEs4(x0, x1, ty_Bool)
new_esEs4(x0, x1, ty_Integer)
new_esEs4(x0, x1, ty_Char)
new_esEs4(x0, x1, app(app(ty_Either, x2), x3))
new_esEs4(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs4(x0, x1, ty_@0)
new_esEs4(x0, x1, ty_Double)
new_esEs4(x0, x1, ty_Ordering)
new_esEs4(x0, x1, ty_Float)
new_esEs4(x0, x1, app(ty_[], x2))
new_esEs4(x0, x1, app(ty_Ratio, x2))
new_esEs4(x0, x1, ty_Int)
new_esEs4(x0, x1, app(ty_Maybe, x2))
new_esEs4(x0, x1, app(app(ty_@2, x2), x3))



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
                ↳ DependencyGraphProof
                  ↳ AND
                    ↳ QDP
                      ↳ UsableRulesProof
                        ↳ QDP
                          ↳ QReductionProof
QDP
                              ↳ QDPSizeChangeProof
                    ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_lookup10(yu22, yu23, yu24, yu25, False, bg, bh, ca) → new_lookup(Right(yu22), yu25, bg, bh, ca)
new_lookup(Right(yu30), :(@2(Right(yu4000), yu401), yu41), bd, be, bf) → new_lookup10(yu30, yu4000, yu401, yu41, new_esEs5(yu30, yu4000, bf), bd, be, bf)
new_lookup(Right(yu30), :(@2(Left(yu4000), yu401), yu41), bd, be, bf) → new_lookup(Right(yu30), yu41, bd, be, bf)

The TRS R consists of the following rules:

new_esEs5(yu30, yu4000, ty_Int) → new_esEs12(yu30, yu4000)
new_esEs5(yu30, yu4000, ty_Ordering) → new_esEs9(yu30, yu4000)
new_esEs5(yu30, yu4000, app(ty_Ratio, bbc)) → new_esEs8(yu30, yu4000, bbc)
new_esEs5(yu30, yu4000, app(ty_Maybe, bcb)) → new_esEs6(yu30, yu4000, bcb)
new_esEs5(yu30, yu4000, ty_Char) → new_esEs7(yu30, yu4000)
new_esEs5(yu30, yu4000, app(app(app(ty_@3, bbf), bbg), bbh)) → new_esEs13(yu30, yu4000, bbf, bbg, bbh)
new_esEs5(yu30, yu4000, ty_Bool) → new_esEs18(yu30, yu4000)
new_esEs5(yu30, yu4000, app(app(ty_@2, bcc), bcd)) → new_esEs19(yu30, yu4000, bcc, bcd)
new_esEs5(yu30, yu4000, ty_@0) → new_esEs16(yu30, yu4000)
new_esEs5(yu30, yu4000, app(app(ty_Either, bbd), bbe)) → new_esEs11(yu30, yu4000, bbd, bbe)
new_esEs5(yu30, yu4000, ty_Integer) → new_esEs10(yu30, yu4000)
new_esEs5(yu30, yu4000, ty_Double) → new_esEs14(yu30, yu4000)
new_esEs5(yu30, yu4000, app(ty_[], bca)) → new_esEs17(yu30, yu4000, bca)
new_esEs5(yu30, yu4000, ty_Float) → new_esEs15(yu30, yu4000)
new_esEs15(Float(yu300, yu301), Float(yu40000, yu40001)) → new_esEs12(new_sr(yu300, yu40000), new_sr(yu301, yu40001))
new_sr(Pos(yu3010), Neg(yu400010)) → Neg(new_primMulNat0(yu3010, yu400010))
new_sr(Neg(yu3010), Pos(yu400010)) → Neg(new_primMulNat0(yu3010, yu400010))
new_sr(Neg(yu3010), Neg(yu400010)) → Pos(new_primMulNat0(yu3010, yu400010))
new_sr(Pos(yu3010), Pos(yu400010)) → Pos(new_primMulNat0(yu3010, yu400010))
new_esEs12(yu30, yu4000) → new_primEqInt(yu30, yu4000)
new_primEqInt(Neg(Succ(yu3000)), Pos(yu40000)) → False
new_primEqInt(Pos(Succ(yu3000)), Neg(yu40000)) → False
new_primEqInt(Neg(Zero), Pos(Succ(yu400000))) → False
new_primEqInt(Pos(Zero), Neg(Succ(yu400000))) → False
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_primEqInt(Neg(Succ(yu3000)), Neg(Succ(yu400000))) → new_primEqNat0(yu3000, yu400000)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_primEqInt(Neg(Zero), Neg(Succ(yu400000))) → False
new_primEqInt(Neg(Succ(yu3000)), Neg(Zero)) → False
new_primEqInt(Pos(Succ(yu3000)), Pos(Succ(yu400000))) → new_primEqNat0(yu3000, yu400000)
new_primEqInt(Pos(Zero), Pos(Succ(yu400000))) → False
new_primEqInt(Pos(Succ(yu3000)), Pos(Zero)) → False
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_primEqNat0(Zero, Succ(yu400000)) → False
new_primEqNat0(Succ(yu3000), Zero) → False
new_primEqNat0(Zero, Zero) → True
new_primEqNat0(Succ(yu3000), Succ(yu400000)) → new_primEqNat0(yu3000, yu400000)
new_primMulNat0(Zero, Zero) → Zero
new_primMulNat0(Succ(yu30100), Zero) → Zero
new_primMulNat0(Zero, Succ(yu4000100)) → Zero
new_primMulNat0(Succ(yu30100), Succ(yu4000100)) → new_primPlusNat0(new_primMulNat0(yu30100, Succ(yu4000100)), yu4000100)
new_primPlusNat0(Zero, yu4000100) → Succ(yu4000100)
new_primPlusNat0(Succ(yu400), yu4000100) → Succ(Succ(new_primPlusNat1(yu400, yu4000100)))
new_primPlusNat1(Succ(yu4000), Succ(yu40001000)) → Succ(Succ(new_primPlusNat1(yu4000, yu40001000)))
new_primPlusNat1(Succ(yu4000), Zero) → Succ(yu4000)
new_primPlusNat1(Zero, Succ(yu40001000)) → Succ(yu40001000)
new_primPlusNat1(Zero, Zero) → Zero
new_esEs17(:(yu300, yu301), :(yu40000, yu40001), hh) → new_asAs(new_esEs23(yu300, yu40000, hh), new_esEs17(yu301, yu40001, hh))
new_esEs17([], [], hh) → True
new_esEs17(:(yu300, yu301), [], hh) → False
new_esEs17([], :(yu40000, yu40001), hh) → False
new_esEs23(yu300, yu40000, app(ty_[], bag)) → new_esEs17(yu300, yu40000, bag)
new_esEs23(yu300, yu40000, ty_Integer) → new_esEs10(yu300, yu40000)
new_esEs23(yu300, yu40000, app(ty_Ratio, baa)) → new_esEs8(yu300, yu40000, baa)
new_esEs23(yu300, yu40000, ty_Ordering) → new_esEs9(yu300, yu40000)
new_esEs23(yu300, yu40000, app(app(ty_Either, bab), bac)) → new_esEs11(yu300, yu40000, bab, bac)
new_esEs23(yu300, yu40000, ty_Char) → new_esEs7(yu300, yu40000)
new_esEs23(yu300, yu40000, ty_Double) → new_esEs14(yu300, yu40000)
new_esEs23(yu300, yu40000, ty_@0) → new_esEs16(yu300, yu40000)
new_esEs23(yu300, yu40000, app(app(app(ty_@3, bad), bae), baf)) → new_esEs13(yu300, yu40000, bad, bae, baf)
new_esEs23(yu300, yu40000, ty_Float) → new_esEs15(yu300, yu40000)
new_esEs23(yu300, yu40000, app(ty_Maybe, bah)) → new_esEs6(yu300, yu40000, bah)
new_esEs23(yu300, yu40000, ty_Bool) → new_esEs18(yu300, yu40000)
new_esEs23(yu300, yu40000, ty_Int) → new_esEs12(yu300, yu40000)
new_esEs23(yu300, yu40000, app(app(ty_@2, bba), bbb)) → new_esEs19(yu300, yu40000, bba, bbb)
new_asAs(False, yu39) → False
new_asAs(True, yu39) → yu39
new_esEs19(@2(yu300, yu301), @2(yu40000, yu40001), bch, bda) → new_asAs(new_esEs24(yu300, yu40000, bch), new_esEs25(yu301, yu40001, bda))
new_esEs24(yu300, yu40000, app(ty_[], bdh)) → new_esEs17(yu300, yu40000, bdh)
new_esEs24(yu300, yu40000, ty_Char) → new_esEs7(yu300, yu40000)
new_esEs24(yu300, yu40000, app(ty_Ratio, bdb)) → new_esEs8(yu300, yu40000, bdb)
new_esEs24(yu300, yu40000, ty_Int) → new_esEs12(yu300, yu40000)
new_esEs24(yu300, yu40000, ty_Integer) → new_esEs10(yu300, yu40000)
new_esEs24(yu300, yu40000, ty_Bool) → new_esEs18(yu300, yu40000)
new_esEs24(yu300, yu40000, app(app(app(ty_@3, bde), bdf), bdg)) → new_esEs13(yu300, yu40000, bde, bdf, bdg)
new_esEs24(yu300, yu40000, ty_Ordering) → new_esEs9(yu300, yu40000)
new_esEs24(yu300, yu40000, ty_@0) → new_esEs16(yu300, yu40000)
new_esEs24(yu300, yu40000, app(ty_Maybe, bea)) → new_esEs6(yu300, yu40000, bea)
new_esEs24(yu300, yu40000, app(app(ty_Either, bdc), bdd)) → new_esEs11(yu300, yu40000, bdc, bdd)
new_esEs24(yu300, yu40000, app(app(ty_@2, beb), bec)) → new_esEs19(yu300, yu40000, beb, bec)
new_esEs24(yu300, yu40000, ty_Float) → new_esEs15(yu300, yu40000)
new_esEs24(yu300, yu40000, ty_Double) → new_esEs14(yu300, yu40000)
new_esEs25(yu301, yu40001, ty_Float) → new_esEs15(yu301, yu40001)
new_esEs25(yu301, yu40001, ty_Integer) → new_esEs10(yu301, yu40001)
new_esEs25(yu301, yu40001, ty_Double) → new_esEs14(yu301, yu40001)
new_esEs25(yu301, yu40001, app(ty_Maybe, bfc)) → new_esEs6(yu301, yu40001, bfc)
new_esEs25(yu301, yu40001, ty_Int) → new_esEs12(yu301, yu40001)
new_esEs25(yu301, yu40001, ty_@0) → new_esEs16(yu301, yu40001)
new_esEs25(yu301, yu40001, ty_Bool) → new_esEs18(yu301, yu40001)
new_esEs25(yu301, yu40001, app(ty_Ratio, bed)) → new_esEs8(yu301, yu40001, bed)
new_esEs25(yu301, yu40001, ty_Char) → new_esEs7(yu301, yu40001)
new_esEs25(yu301, yu40001, app(ty_[], bfb)) → new_esEs17(yu301, yu40001, bfb)
new_esEs25(yu301, yu40001, app(app(app(ty_@3, beg), beh), bfa)) → new_esEs13(yu301, yu40001, beg, beh, bfa)
new_esEs25(yu301, yu40001, ty_Ordering) → new_esEs9(yu301, yu40001)
new_esEs25(yu301, yu40001, app(app(ty_Either, bee), bef)) → new_esEs11(yu301, yu40001, bee, bef)
new_esEs25(yu301, yu40001, app(app(ty_@2, bfd), bfe)) → new_esEs19(yu301, yu40001, bfd, bfe)
new_esEs11(Right(yu300), Right(yu40000), bcf, app(ty_[], bhf)) → new_esEs17(yu300, yu40000, bhf)
new_esEs11(Right(yu300), Right(yu40000), bcf, ty_Integer) → new_esEs10(yu300, yu40000)
new_esEs6(Just(yu300), Just(yu40000), app(ty_Maybe, dc)) → new_esEs6(yu300, yu40000, dc)
new_esEs11(Left(yu300), Left(yu40000), app(app(ty_Either, bfg), bfh), bcg) → new_esEs11(yu300, yu40000, bfg, bfh)
new_esEs11(Right(yu300), Right(yu40000), bcf, app(app(ty_Either, bha), bhb)) → new_esEs11(yu300, yu40000, bha, bhb)
new_esEs11(Right(yu300), Right(yu40000), bcf, app(ty_Maybe, bhg)) → new_esEs6(yu300, yu40000, bhg)
new_esEs11(Left(yu300), Left(yu40000), app(ty_Maybe, bge), bcg) → new_esEs6(yu300, yu40000, bge)
new_esEs6(Just(yu300), Just(yu40000), app(app(ty_Either, cd), ce)) → new_esEs11(yu300, yu40000, cd, ce)
new_esEs11(Left(yu300), Left(yu40000), ty_Char, bcg) → new_esEs7(yu300, yu40000)
new_esEs11(Right(yu300), Right(yu40000), bcf, ty_Char) → new_esEs7(yu300, yu40000)
new_esEs11(Right(yu300), Right(yu40000), bcf, app(ty_Ratio, bgh)) → new_esEs8(yu300, yu40000, bgh)
new_esEs11(Right(yu300), Right(yu40000), bcf, app(app(ty_@2, bhh), caa)) → new_esEs19(yu300, yu40000, bhh, caa)
new_esEs11(Right(yu300), Right(yu40000), bcf, app(app(app(ty_@3, bhc), bhd), bhe)) → new_esEs13(yu300, yu40000, bhc, bhd, bhe)
new_esEs11(Left(yu300), Left(yu40000), ty_Float, bcg) → new_esEs15(yu300, yu40000)
new_esEs11(Right(yu300), Right(yu40000), bcf, ty_Ordering) → new_esEs9(yu300, yu40000)
new_esEs11(Left(yu300), Left(yu40000), ty_Double, bcg) → new_esEs14(yu300, yu40000)
new_esEs11(Left(yu300), Left(yu40000), app(ty_[], bgd), bcg) → new_esEs17(yu300, yu40000, bgd)
new_esEs11(Right(yu300), Right(yu40000), bcf, ty_Double) → new_esEs14(yu300, yu40000)
new_esEs11(Left(yu300), Left(yu40000), ty_Integer, bcg) → new_esEs10(yu300, yu40000)
new_esEs11(Left(yu300), Left(yu40000), app(app(ty_@2, bgf), bgg), bcg) → new_esEs19(yu300, yu40000, bgf, bgg)
new_esEs11(Right(yu300), Right(yu40000), bcf, ty_Float) → new_esEs15(yu300, yu40000)
new_esEs11(Left(yu300), Left(yu40000), ty_Bool, bcg) → new_esEs18(yu300, yu40000)
new_esEs11(Left(yu300), Left(yu40000), app(ty_Ratio, bff), bcg) → new_esEs8(yu300, yu40000, bff)
new_esEs11(Right(yu300), Right(yu40000), bcf, ty_@0) → new_esEs16(yu300, yu40000)
new_esEs11(Left(yu300), Left(yu40000), ty_@0, bcg) → new_esEs16(yu300, yu40000)
new_esEs11(Left(yu300), Left(yu40000), ty_Ordering, bcg) → new_esEs9(yu300, yu40000)
new_esEs11(Right(yu300), Right(yu40000), bcf, ty_Bool) → new_esEs18(yu300, yu40000)
new_esEs11(Left(yu300), Left(yu40000), app(app(app(ty_@3, bga), bgb), bgc), bcg) → new_esEs13(yu300, yu40000, bga, bgb, bgc)
new_esEs11(Right(yu300), Right(yu40000), bcf, ty_Int) → new_esEs12(yu300, yu40000)
new_esEs11(Left(yu300), Left(yu40000), ty_Int, bcg) → new_esEs12(yu300, yu40000)
new_esEs11(Left(yu300), Right(yu40000), bcf, bcg) → False
new_esEs11(Right(yu300), Left(yu40000), bcf, bcg) → False
new_esEs13(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), df, dg, dh) → new_asAs(new_esEs20(yu300, yu40000, df), new_asAs(new_esEs21(yu301, yu40001, dg), new_esEs22(yu302, yu40002, dh)))
new_esEs20(yu300, yu40000, ty_@0) → new_esEs16(yu300, yu40000)
new_esEs20(yu300, yu40000, ty_Bool) → new_esEs18(yu300, yu40000)
new_esEs20(yu300, yu40000, ty_Integer) → new_esEs10(yu300, yu40000)
new_esEs20(yu300, yu40000, app(app(ty_Either, eb), ec)) → new_esEs11(yu300, yu40000, eb, ec)
new_esEs20(yu300, yu40000, app(app(ty_@2, fa), fb)) → new_esEs19(yu300, yu40000, fa, fb)
new_esEs20(yu300, yu40000, app(ty_[], eg)) → new_esEs17(yu300, yu40000, eg)
new_esEs20(yu300, yu40000, app(ty_Maybe, eh)) → new_esEs6(yu300, yu40000, eh)
new_esEs20(yu300, yu40000, app(ty_Ratio, ea)) → new_esEs8(yu300, yu40000, ea)
new_esEs20(yu300, yu40000, ty_Ordering) → new_esEs9(yu300, yu40000)
new_esEs20(yu300, yu40000, ty_Int) → new_esEs12(yu300, yu40000)
new_esEs20(yu300, yu40000, ty_Char) → new_esEs7(yu300, yu40000)
new_esEs20(yu300, yu40000, app(app(app(ty_@3, ed), ee), ef)) → new_esEs13(yu300, yu40000, ed, ee, ef)
new_esEs20(yu300, yu40000, ty_Double) → new_esEs14(yu300, yu40000)
new_esEs20(yu300, yu40000, ty_Float) → new_esEs15(yu300, yu40000)
new_esEs21(yu301, yu40001, ty_Float) → new_esEs15(yu301, yu40001)
new_esEs21(yu301, yu40001, app(app(ty_Either, fd), ff)) → new_esEs11(yu301, yu40001, fd, ff)
new_esEs21(yu301, yu40001, app(app(ty_@2, gd), ge)) → new_esEs19(yu301, yu40001, gd, ge)
new_esEs21(yu301, yu40001, app(ty_[], gb)) → new_esEs17(yu301, yu40001, gb)
new_esEs21(yu301, yu40001, ty_Int) → new_esEs12(yu301, yu40001)
new_esEs21(yu301, yu40001, ty_Integer) → new_esEs10(yu301, yu40001)
new_esEs21(yu301, yu40001, app(app(app(ty_@3, fg), fh), ga)) → new_esEs13(yu301, yu40001, fg, fh, ga)
new_esEs21(yu301, yu40001, ty_Bool) → new_esEs18(yu301, yu40001)
new_esEs21(yu301, yu40001, ty_Ordering) → new_esEs9(yu301, yu40001)
new_esEs21(yu301, yu40001, app(ty_Ratio, fc)) → new_esEs8(yu301, yu40001, fc)
new_esEs21(yu301, yu40001, ty_@0) → new_esEs16(yu301, yu40001)
new_esEs21(yu301, yu40001, ty_Double) → new_esEs14(yu301, yu40001)
new_esEs21(yu301, yu40001, app(ty_Maybe, gc)) → new_esEs6(yu301, yu40001, gc)
new_esEs21(yu301, yu40001, ty_Char) → new_esEs7(yu301, yu40001)
new_esEs22(yu302, yu40002, ty_Bool) → new_esEs18(yu302, yu40002)
new_esEs22(yu302, yu40002, ty_Ordering) → new_esEs9(yu302, yu40002)
new_esEs22(yu302, yu40002, ty_@0) → new_esEs16(yu302, yu40002)
new_esEs22(yu302, yu40002, ty_Char) → new_esEs7(yu302, yu40002)
new_esEs22(yu302, yu40002, app(ty_Ratio, gf)) → new_esEs8(yu302, yu40002, gf)
new_esEs22(yu302, yu40002, app(ty_Maybe, he)) → new_esEs6(yu302, yu40002, he)
new_esEs22(yu302, yu40002, ty_Integer) → new_esEs10(yu302, yu40002)
new_esEs22(yu302, yu40002, ty_Double) → new_esEs14(yu302, yu40002)
new_esEs22(yu302, yu40002, app(ty_[], hd)) → new_esEs17(yu302, yu40002, hd)
new_esEs22(yu302, yu40002, app(app(ty_@2, hf), hg)) → new_esEs19(yu302, yu40002, hf, hg)
new_esEs22(yu302, yu40002, ty_Float) → new_esEs15(yu302, yu40002)
new_esEs22(yu302, yu40002, app(app(app(ty_@3, ha), hb), hc)) → new_esEs13(yu302, yu40002, ha, hb, hc)
new_esEs22(yu302, yu40002, ty_Int) → new_esEs12(yu302, yu40002)
new_esEs22(yu302, yu40002, app(app(ty_Either, gg), gh)) → new_esEs11(yu302, yu40002, gg, gh)
new_esEs14(Double(yu300, yu301), Double(yu40000, yu40001)) → new_esEs12(new_sr(yu300, yu40000), new_sr(yu301, yu40001))
new_esEs10(Integer(yu300), Integer(yu40000)) → new_primEqInt(yu300, yu40000)
new_esEs6(Just(yu300), Just(yu40000), ty_@0) → new_esEs16(yu300, yu40000)
new_esEs6(Just(yu300), Just(yu40000), ty_Ordering) → new_esEs9(yu300, yu40000)
new_esEs6(Just(yu300), Just(yu40000), ty_Float) → new_esEs15(yu300, yu40000)
new_esEs6(Just(yu300), Just(yu40000), app(app(ty_@2, dd), de)) → new_esEs19(yu300, yu40000, dd, de)
new_esEs6(Just(yu300), Just(yu40000), app(ty_Ratio, cc)) → new_esEs8(yu300, yu40000, cc)
new_esEs6(Just(yu300), Just(yu40000), ty_Int) → new_esEs12(yu300, yu40000)
new_esEs6(Just(yu300), Just(yu40000), app(ty_[], db)) → new_esEs17(yu300, yu40000, db)
new_esEs6(Just(yu300), Just(yu40000), app(app(app(ty_@3, cf), cg), da)) → new_esEs13(yu300, yu40000, cf, cg, da)
new_esEs6(Just(yu300), Just(yu40000), ty_Bool) → new_esEs18(yu300, yu40000)
new_esEs6(Just(yu300), Just(yu40000), ty_Double) → new_esEs14(yu300, yu40000)
new_esEs6(Nothing, Nothing, cb) → True
new_esEs6(Just(yu300), Nothing, cb) → False
new_esEs6(Nothing, Just(yu40000), cb) → False
new_esEs6(Just(yu300), Just(yu40000), ty_Char) → new_esEs7(yu300, yu40000)
new_esEs6(Just(yu300), Just(yu40000), ty_Integer) → new_esEs10(yu300, yu40000)
new_esEs7(Char(yu300), Char(yu40000)) → new_primEqNat0(yu300, yu40000)
new_esEs18(True, True) → True
new_esEs18(True, False) → False
new_esEs18(False, True) → False
new_esEs18(False, False) → True
new_esEs8(:%(yu300, yu301), :%(yu40000, yu40001), bce) → new_asAs(new_esEs26(yu300, yu40000, bce), new_esEs27(yu301, yu40001, bce))
new_esEs26(yu300, yu40000, ty_Int) → new_esEs12(yu300, yu40000)
new_esEs26(yu300, yu40000, ty_Integer) → new_esEs10(yu300, yu40000)
new_esEs27(yu301, yu40001, ty_Integer) → new_esEs10(yu301, yu40001)
new_esEs27(yu301, yu40001, ty_Int) → new_esEs12(yu301, yu40001)
new_esEs9(GT, LT) → False
new_esEs9(LT, GT) → False
new_esEs9(GT, GT) → True
new_esEs9(GT, EQ) → False
new_esEs9(EQ, GT) → False
new_esEs9(EQ, EQ) → True
new_esEs9(EQ, LT) → False
new_esEs9(LT, EQ) → False
new_esEs9(LT, LT) → True
new_esEs16(@0, @0) → True

The set Q consists of the following terms:

new_esEs23(x0, x1, ty_Int)
new_esEs21(x0, x1, ty_Int)
new_esEs9(GT, GT)
new_esEs25(x0, x1, ty_Double)
new_esEs27(x0, x1, ty_Int)
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_esEs22(x0, x1, ty_Ordering)
new_esEs5(x0, x1, ty_Char)
new_primEqInt(Neg(Zero), Pos(Zero))
new_primEqInt(Pos(Zero), Neg(Zero))
new_esEs22(x0, x1, ty_Char)
new_esEs5(x0, x1, ty_Float)
new_esEs25(x0, x1, ty_Integer)
new_esEs20(x0, x1, ty_Bool)
new_esEs11(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs11(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs10(Integer(x0), Integer(x1))
new_esEs6(Nothing, Just(x0), x1)
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs18(False, True)
new_esEs18(True, False)
new_esEs5(x0, x1, ty_Bool)
new_esEs6(Just(x0), Just(x1), ty_Double)
new_esEs9(EQ, EQ)
new_esEs25(x0, x1, ty_Bool)
new_esEs11(Right(x0), Right(x1), x2, ty_Int)
new_esEs24(x0, x1, ty_Ordering)
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs11(Right(x0), Right(x1), x2, ty_Integer)
new_esEs6(Just(x0), Nothing, x1)
new_esEs11(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs19(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs22(x0, x1, ty_@0)
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs6(Just(x0), Just(x1), ty_@0)
new_esEs5(x0, x1, app(ty_Maybe, x2))
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs11(Left(x0), Left(x1), ty_Float, x2)
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_esEs11(Right(x0), Right(x1), x2, ty_Char)
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_sr(Neg(x0), Neg(x1))
new_esEs22(x0, x1, ty_Int)
new_esEs17([], :(x0, x1), x2)
new_esEs18(True, True)
new_esEs6(Just(x0), Just(x1), ty_Integer)
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_esEs20(x0, x1, ty_Char)
new_esEs7(Char(x0), Char(x1))
new_esEs5(x0, x1, ty_@0)
new_esEs9(LT, GT)
new_esEs9(GT, LT)
new_esEs11(Right(x0), Right(x1), x2, ty_Ordering)
new_primPlusNat0(Zero, x0)
new_esEs25(x0, x1, app(ty_[], x2))
new_esEs24(x0, x1, ty_Bool)
new_esEs16(@0, @0)
new_esEs6(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs21(x0, x1, ty_Ordering)
new_esEs6(Just(x0), Just(x1), ty_Float)
new_esEs23(x0, x1, ty_Ordering)
new_esEs9(GT, EQ)
new_esEs9(EQ, GT)
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_asAs(False, x0)
new_esEs5(x0, x1, ty_Double)
new_esEs23(x0, x1, ty_Char)
new_esEs20(x0, x1, ty_Integer)
new_esEs6(Just(x0), Just(x1), ty_Bool)
new_esEs17(:(x0, x1), [], x2)
new_esEs5(x0, x1, ty_Ordering)
new_primPlusNat1(Zero, Succ(x0))
new_esEs11(Left(x0), Left(x1), ty_Int, x2)
new_esEs24(x0, x1, ty_Char)
new_esEs25(x0, x1, ty_Char)
new_esEs20(x0, x1, app(ty_[], x2))
new_esEs20(x0, x1, ty_Int)
new_esEs5(x0, x1, app(ty_Ratio, x2))
new_esEs26(x0, x1, ty_Int)
new_esEs23(x0, x1, ty_Bool)
new_primEqNat0(Zero, Zero)
new_esEs23(x0, x1, ty_Integer)
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_primMulNat0(Zero, Succ(x0))
new_esEs11(Left(x0), Left(x1), ty_@0, x2)
new_primEqNat0(Succ(x0), Zero)
new_esEs20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs24(x0, x1, ty_Float)
new_esEs6(Just(x0), Just(x1), ty_Int)
new_esEs22(x0, x1, ty_Bool)
new_primPlusNat0(Succ(x0), x1)
new_esEs6(Nothing, Nothing, x0)
new_esEs6(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs11(Right(x0), Right(x1), x2, ty_@0)
new_esEs11(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_esEs21(x0, x1, ty_Float)
new_primMulNat0(Zero, Zero)
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_asAs(True, x0)
new_esEs20(x0, x1, ty_Ordering)
new_esEs5(x0, x1, ty_Integer)
new_esEs21(x0, x1, app(ty_Ratio, x2))
new_esEs21(x0, x1, ty_@0)
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs5(x0, x1, ty_Int)
new_esEs6(Just(x0), Just(x1), ty_Char)
new_esEs11(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs22(x0, x1, app(ty_[], x2))
new_esEs13(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs11(Left(x0), Left(x1), ty_Bool, x2)
new_esEs20(x0, x1, ty_Double)
new_primMulNat0(Succ(x0), Zero)
new_esEs6(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs11(Right(x0), Right(x1), x2, ty_Bool)
new_esEs11(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_sr(Pos(x0), Pos(x1))
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_esEs20(x0, x1, ty_Float)
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs22(x0, x1, ty_Double)
new_esEs11(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs12(x0, x1)
new_esEs5(x0, x1, app(ty_[], x2))
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs11(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs9(LT, EQ)
new_esEs9(EQ, LT)
new_esEs15(Float(x0, x1), Float(x2, x3))
new_esEs11(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs23(x0, x1, ty_Double)
new_esEs6(Just(x0), Just(x1), app(ty_[], x2))
new_esEs25(x0, x1, ty_Int)
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs17(:(x0, x1), :(x2, x3), x4)
new_esEs23(x0, x1, ty_Float)
new_esEs25(x0, x1, ty_Ordering)
new_esEs11(Left(x0), Left(x1), ty_Double, x2)
new_esEs24(x0, x1, app(ty_[], x2))
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs18(False, False)
new_esEs21(x0, x1, ty_Double)
new_esEs20(x0, x1, app(ty_Ratio, x2))
new_esEs24(x0, x1, ty_Int)
new_esEs21(x0, x1, app(ty_[], x2))
new_esEs22(x0, x1, ty_Integer)
new_esEs20(x0, x1, ty_@0)
new_esEs23(x0, x1, ty_@0)
new_esEs11(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs20(x0, x1, app(app(ty_Either, x2), x3))
new_esEs11(Left(x0), Left(x1), ty_Integer, x2)
new_primPlusNat1(Succ(x0), Zero)
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs6(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs23(x0, x1, app(ty_[], x2))
new_primMulNat0(Succ(x0), Succ(x1))
new_primPlusNat1(Zero, Zero)
new_esEs24(x0, x1, ty_Double)
new_esEs17([], [], x0)
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs27(x0, x1, ty_Integer)
new_esEs22(x0, x1, ty_Float)
new_esEs26(x0, x1, ty_Integer)
new_esEs24(x0, x1, app(ty_Maybe, x2))
new_esEs5(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs25(x0, x1, ty_@0)
new_esEs5(x0, x1, app(app(ty_Either, x2), x3))
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs11(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs11(Right(x0), Right(x1), x2, ty_Double)
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_esEs6(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs6(Just(x0), Just(x1), ty_Ordering)
new_esEs11(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs21(x0, x1, ty_Char)
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs11(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_esEs25(x0, x1, ty_Float)
new_esEs11(Left(x0), Right(x1), x2, x3)
new_esEs11(Right(x0), Left(x1), x2, x3)
new_esEs24(x0, x1, ty_@0)
new_esEs5(x0, x1, app(app(ty_@2, x2), x3))
new_primEqNat0(Zero, Succ(x0))
new_esEs8(:%(x0, x1), :%(x2, x3), x4)
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_esEs21(x0, x1, ty_Bool)
new_esEs24(x0, x1, ty_Integer)
new_esEs11(Right(x0), Right(x1), x2, ty_Float)
new_esEs11(Left(x0), Left(x1), ty_Char, x2)
new_esEs20(x0, x1, app(ty_Maybe, x2))
new_esEs9(LT, LT)
new_esEs14(Double(x0, x1), Double(x2, x3))
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_sr(Neg(x0), Pos(x1))
new_sr(Pos(x0), Neg(x1))
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_esEs20(x0, x1, app(app(ty_@2, x2), x3))
new_esEs21(x0, x1, ty_Integer)
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
                ↳ DependencyGraphProof
                  ↳ AND
                    ↳ QDP
QDP
                      ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

new_lookup(Left(yu30), :(@2(Right(yu4000), yu401), yu41), bd, be, bf) → new_lookup(Left(yu30), yu41, bd, be, bf)
new_lookup1(yu11, yu12, yu13, yu14, False, ba, bb, bc) → new_lookup(Left(yu11), yu14, ba, bb, bc)
new_lookup(Left(yu30), :(@2(Left(yu4000), yu401), yu41), bd, be, bf) → new_lookup1(yu30, yu4000, yu401, yu41, new_esEs4(yu30, yu4000, be), bd, be, bf)

The TRS R consists of the following rules:

new_esEs21(yu301, yu40001, ty_Float) → new_esEs15(yu301, yu40001)
new_esEs22(yu302, yu40002, ty_Bool) → new_esEs18(yu302, yu40002)
new_primPlusNat1(Succ(yu4000), Succ(yu40001000)) → Succ(Succ(new_primPlusNat1(yu4000, yu40001000)))
new_esEs4(yu30, yu4000, ty_@0) → new_esEs16(yu30, yu4000)
new_primEqInt(Neg(Succ(yu3000)), Pos(yu40000)) → False
new_primEqInt(Pos(Succ(yu3000)), Neg(yu40000)) → False
new_esEs5(yu30, yu4000, ty_Int) → new_esEs12(yu30, yu4000)
new_esEs20(yu300, yu40000, ty_@0) → new_esEs16(yu300, yu40000)
new_esEs9(GT, LT) → False
new_esEs9(LT, GT) → False
new_esEs7(Char(yu300), Char(yu40000)) → new_primEqNat0(yu300, yu40000)
new_esEs11(Right(yu300), Right(yu40000), bcf, app(ty_[], bhf)) → new_esEs17(yu300, yu40000, bhf)
new_esEs5(yu30, yu4000, ty_Ordering) → new_esEs9(yu30, yu4000)
new_primEqInt(Neg(Zero), Pos(Succ(yu400000))) → False
new_primEqInt(Pos(Zero), Neg(Succ(yu400000))) → False
new_esEs4(yu30, yu4000, app(app(app(ty_@3, df), dg), dh)) → new_esEs13(yu30, yu4000, df, dg, dh)
new_esEs5(yu30, yu4000, app(ty_Ratio, bbc)) → new_esEs8(yu30, yu4000, bbc)
new_esEs21(yu301, yu40001, app(app(ty_Either, fd), ff)) → new_esEs11(yu301, yu40001, fd, ff)
new_esEs17(:(yu300, yu301), :(yu40000, yu40001), hh) → new_asAs(new_esEs23(yu300, yu40000, hh), new_esEs17(yu301, yu40001, hh))
new_esEs11(Right(yu300), Right(yu40000), bcf, ty_Integer) → new_esEs10(yu300, yu40000)
new_esEs11(Right(yu300), Right(yu40000), bcf, app(ty_Maybe, bhg)) → new_esEs6(yu300, yu40000, bhg)
new_esEs21(yu301, yu40001, app(app(ty_@2, gd), ge)) → new_esEs19(yu301, yu40001, gd, ge)
new_esEs4(yu30, yu4000, app(app(ty_Either, bcf), bcg)) → new_esEs11(yu30, yu4000, bcf, bcg)
new_esEs22(yu302, yu40002, ty_Ordering) → new_esEs9(yu302, yu40002)
new_esEs22(yu302, yu40002, ty_@0) → new_esEs16(yu302, yu40002)
new_esEs23(yu300, yu40000, app(ty_[], bag)) → new_esEs17(yu300, yu40000, bag)
new_esEs25(yu301, yu40001, ty_Float) → new_esEs15(yu301, yu40001)
new_esEs13(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), df, dg, dh) → new_asAs(new_esEs20(yu300, yu40000, df), new_asAs(new_esEs21(yu301, yu40001, dg), new_esEs22(yu302, yu40002, dh)))
new_esEs6(Just(yu300), Just(yu40000), ty_@0) → new_esEs16(yu300, yu40000)
new_esEs21(yu301, yu40001, app(ty_[], gb)) → new_esEs17(yu301, yu40001, gb)
new_primMulNat0(Zero, Zero) → Zero
new_esEs21(yu301, yu40001, ty_Int) → new_esEs12(yu301, yu40001)
new_esEs22(yu302, yu40002, ty_Char) → new_esEs7(yu302, yu40002)
new_esEs4(yu30, yu4000, app(ty_[], hh)) → new_esEs17(yu30, yu4000, hh)
new_esEs22(yu302, yu40002, app(ty_Ratio, gf)) → new_esEs8(yu302, yu40002, gf)
new_esEs27(yu301, yu40001, ty_Integer) → new_esEs10(yu301, yu40001)
new_esEs4(yu30, yu4000, ty_Int) → new_esEs12(yu30, yu4000)
new_esEs4(yu30, yu4000, app(ty_Maybe, cb)) → new_esEs6(yu30, yu4000, cb)
new_primPlusNat0(Zero, yu4000100) → Succ(yu4000100)
new_esEs20(yu300, yu40000, ty_Bool) → new_esEs18(yu300, yu40000)
new_esEs9(GT, GT) → True
new_esEs4(yu30, yu4000, ty_Float) → new_esEs15(yu30, yu4000)
new_esEs6(Just(yu300), Just(yu40000), ty_Ordering) → new_esEs9(yu300, yu40000)
new_esEs20(yu300, yu40000, ty_Integer) → new_esEs10(yu300, yu40000)
new_esEs11(Left(yu300), Left(yu40000), ty_Char, bcg) → new_esEs7(yu300, yu40000)
new_esEs25(yu301, yu40001, ty_Integer) → new_esEs10(yu301, yu40001)
new_esEs5(yu30, yu4000, app(ty_Maybe, bcb)) → new_esEs6(yu30, yu4000, bcb)
new_sr(Pos(yu3010), Neg(yu400010)) → Neg(new_primMulNat0(yu3010, yu400010))
new_sr(Neg(yu3010), Pos(yu400010)) → Neg(new_primMulNat0(yu3010, yu400010))
new_esEs24(yu300, yu40000, app(ty_[], bdh)) → new_esEs17(yu300, yu40000, bdh)
new_esEs6(Just(yu300), Just(yu40000), app(app(ty_Either, cd), ce)) → new_esEs11(yu300, yu40000, cd, ce)
new_esEs6(Just(yu300), Just(yu40000), ty_Float) → new_esEs15(yu300, yu40000)
new_esEs11(Right(yu300), Right(yu40000), bcf, app(app(ty_Either, bha), bhb)) → new_esEs11(yu300, yu40000, bha, bhb)
new_esEs24(yu300, yu40000, ty_Char) → new_esEs7(yu300, yu40000)
new_esEs22(yu302, yu40002, app(ty_Maybe, he)) → new_esEs6(yu302, yu40002, he)
new_esEs24(yu300, yu40000, app(ty_Ratio, bdb)) → new_esEs8(yu300, yu40000, bdb)
new_esEs5(yu30, yu4000, ty_Char) → new_esEs7(yu30, yu4000)
new_esEs20(yu300, yu40000, app(app(ty_Either, eb), ec)) → new_esEs11(yu300, yu40000, eb, ec)
new_esEs23(yu300, yu40000, ty_Integer) → new_esEs10(yu300, yu40000)
new_esEs25(yu301, yu40001, ty_Double) → new_esEs14(yu301, yu40001)
new_esEs23(yu300, yu40000, app(ty_Ratio, baa)) → new_esEs8(yu300, yu40000, baa)
new_esEs11(Right(yu300), Right(yu40000), bcf, ty_Char) → new_esEs7(yu300, yu40000)
new_esEs11(Right(yu300), Right(yu40000), bcf, app(ty_Ratio, bgh)) → new_esEs8(yu300, yu40000, bgh)
new_esEs23(yu300, yu40000, ty_Ordering) → new_esEs9(yu300, yu40000)
new_esEs11(Left(yu300), Left(yu40000), app(app(ty_Either, bfg), bfh), bcg) → new_esEs11(yu300, yu40000, bfg, bfh)
new_esEs22(yu302, yu40002, ty_Integer) → new_esEs10(yu302, yu40002)
new_primEqNat0(Zero, Succ(yu400000)) → False
new_primEqNat0(Succ(yu3000), Zero) → False
new_esEs25(yu301, yu40001, app(ty_Maybe, bfc)) → new_esEs6(yu301, yu40001, bfc)
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_esEs22(yu302, yu40002, ty_Double) → new_esEs14(yu302, yu40002)
new_esEs20(yu300, yu40000, app(app(ty_@2, fa), fb)) → new_esEs19(yu300, yu40000, fa, fb)
new_esEs21(yu301, yu40001, ty_Integer) → new_esEs10(yu301, yu40001)
new_esEs10(Integer(yu300), Integer(yu40000)) → new_primEqInt(yu300, yu40000)
new_esEs25(yu301, yu40001, ty_Int) → new_esEs12(yu301, yu40001)
new_esEs6(Just(yu300), Just(yu40000), app(app(ty_@2, dd), de)) → new_esEs19(yu300, yu40000, dd, de)
new_esEs20(yu300, yu40000, app(ty_[], eg)) → new_esEs17(yu300, yu40000, eg)
new_esEs15(Float(yu300, yu301), Float(yu40000, yu40001)) → new_esEs12(new_sr(yu300, yu40000), new_sr(yu301, yu40001))
new_esEs5(yu30, yu4000, app(app(app(ty_@3, bbf), bbg), bbh)) → new_esEs13(yu30, yu4000, bbf, bbg, bbh)
new_esEs22(yu302, yu40002, app(ty_[], hd)) → new_esEs17(yu302, yu40002, hd)
new_esEs5(yu30, yu4000, ty_Bool) → new_esEs18(yu30, yu4000)
new_esEs11(Right(yu300), Right(yu40000), bcf, app(app(ty_@2, bhh), caa)) → new_esEs19(yu300, yu40000, bhh, caa)
new_esEs4(yu30, yu4000, ty_Double) → new_esEs14(yu30, yu4000)
new_esEs21(yu301, yu40001, app(app(app(ty_@3, fg), fh), ga)) → new_esEs13(yu301, yu40001, fg, fh, ga)
new_esEs23(yu300, yu40000, app(app(ty_Either, bab), bac)) → new_esEs11(yu300, yu40000, bab, bac)
new_esEs6(Just(yu300), Just(yu40000), app(ty_Ratio, cc)) → new_esEs8(yu300, yu40000, cc)
new_esEs12(yu30, yu4000) → new_primEqInt(yu30, yu4000)
new_esEs6(Just(yu300), Just(yu40000), ty_Int) → new_esEs12(yu300, yu40000)
new_esEs9(GT, EQ) → False
new_esEs9(EQ, GT) → False
new_esEs22(yu302, yu40002, app(app(ty_@2, hf), hg)) → new_esEs19(yu302, yu40002, hf, hg)
new_esEs23(yu300, yu40000, ty_Char) → new_esEs7(yu300, yu40000)
new_esEs5(yu30, yu4000, app(app(ty_@2, bcc), bcd)) → new_esEs19(yu30, yu4000, bcc, bcd)
new_esEs5(yu30, yu4000, ty_@0) → new_esEs16(yu30, yu4000)
new_esEs6(Just(yu300), Just(yu40000), app(ty_[], db)) → new_esEs17(yu300, yu40000, db)
new_esEs23(yu300, yu40000, ty_Double) → new_esEs14(yu300, yu40000)
new_esEs6(Just(yu300), Just(yu40000), app(app(app(ty_@3, cf), cg), da)) → new_esEs13(yu300, yu40000, cf, cg, da)
new_esEs22(yu302, yu40002, ty_Float) → new_esEs15(yu302, yu40002)
new_esEs11(Right(yu300), Right(yu40000), bcf, app(app(app(ty_@3, bhc), bhd), bhe)) → new_esEs13(yu300, yu40000, bhc, bhd, bhe)
new_esEs24(yu300, yu40000, ty_Int) → new_esEs12(yu300, yu40000)
new_esEs20(yu300, yu40000, app(ty_Maybe, eh)) → new_esEs6(yu300, yu40000, eh)
new_sr(Neg(yu3010), Neg(yu400010)) → Pos(new_primMulNat0(yu3010, yu400010))
new_esEs21(yu301, yu40001, ty_Bool) → new_esEs18(yu301, yu40001)
new_asAs(False, yu39) → False
new_sr(Pos(yu3010), Pos(yu400010)) → Pos(new_primMulNat0(yu3010, yu400010))
new_esEs23(yu300, yu40000, ty_@0) → new_esEs16(yu300, yu40000)
new_esEs14(Double(yu300, yu301), Double(yu40000, yu40001)) → new_esEs12(new_sr(yu300, yu40000), new_sr(yu301, yu40001))
new_primEqNat0(Zero, Zero) → True
new_esEs6(Just(yu300), Just(yu40000), ty_Bool) → new_esEs18(yu300, yu40000)
new_primMulNat0(Succ(yu30100), Zero) → Zero
new_primMulNat0(Zero, Succ(yu4000100)) → Zero
new_esEs5(yu30, yu4000, app(app(ty_Either, bbd), bbe)) → new_esEs11(yu30, yu4000, bbd, bbe)
new_esEs11(Left(yu300), Left(yu40000), ty_Float, bcg) → new_esEs15(yu300, yu40000)
new_esEs6(Just(yu300), Just(yu40000), app(ty_Maybe, dc)) → new_esEs6(yu300, yu40000, dc)
new_esEs25(yu301, yu40001, ty_@0) → new_esEs16(yu301, yu40001)
new_esEs11(Right(yu300), Right(yu40000), bcf, ty_Ordering) → new_esEs9(yu300, yu40000)
new_esEs25(yu301, yu40001, ty_Bool) → new_esEs18(yu301, yu40001)
new_esEs25(yu301, yu40001, app(ty_Ratio, bed)) → new_esEs8(yu301, yu40001, bed)
new_esEs18(True, True) → True
new_esEs25(yu301, yu40001, ty_Char) → new_esEs7(yu301, yu40001)
new_esEs23(yu300, yu40000, app(app(app(ty_@3, bad), bae), baf)) → new_esEs13(yu300, yu40000, bad, bae, baf)
new_esEs6(Just(yu300), Just(yu40000), ty_Double) → new_esEs14(yu300, yu40000)
new_esEs22(yu302, yu40002, app(app(app(ty_@3, ha), hb), hc)) → new_esEs13(yu302, yu40002, ha, hb, hc)
new_esEs23(yu300, yu40000, ty_Float) → new_esEs15(yu300, yu40000)
new_esEs23(yu300, yu40000, app(ty_Maybe, bah)) → new_esEs6(yu300, yu40000, bah)
new_esEs20(yu300, yu40000, app(ty_Ratio, ea)) → new_esEs8(yu300, yu40000, ea)
new_esEs25(yu301, yu40001, app(ty_[], bfb)) → new_esEs17(yu301, yu40001, bfb)
new_esEs11(Left(yu300), Left(yu40000), ty_Double, bcg) → new_esEs14(yu300, yu40000)
new_esEs26(yu300, yu40000, ty_Int) → new_esEs12(yu300, yu40000)
new_esEs11(Left(yu300), Left(yu40000), app(ty_[], bgd), bcg) → new_esEs17(yu300, yu40000, bgd)
new_esEs16(@0, @0) → True
new_primPlusNat0(Succ(yu400), yu4000100) → Succ(Succ(new_primPlusNat1(yu400, yu4000100)))
new_esEs24(yu300, yu40000, ty_Integer) → new_esEs10(yu300, yu40000)
new_esEs23(yu300, yu40000, ty_Bool) → new_esEs18(yu300, yu40000)
new_esEs11(Right(yu300), Right(yu40000), bcf, ty_Double) → new_esEs14(yu300, yu40000)
new_esEs4(yu30, yu4000, app(ty_Ratio, bce)) → new_esEs8(yu30, yu4000, bce)
new_esEs20(yu300, yu40000, ty_Ordering) → new_esEs9(yu300, yu40000)
new_esEs23(yu300, yu40000, ty_Int) → new_esEs12(yu300, yu40000)
new_esEs21(yu301, yu40001, ty_Ordering) → new_esEs9(yu301, yu40001)
new_esEs25(yu301, yu40001, app(app(app(ty_@3, beg), beh), bfa)) → new_esEs13(yu301, yu40001, beg, beh, bfa)
new_esEs4(yu30, yu4000, ty_Bool) → new_esEs18(yu30, yu4000)
new_esEs4(yu30, yu4000, ty_Integer) → new_esEs10(yu30, yu4000)
new_esEs9(EQ, EQ) → True
new_primEqInt(Neg(Succ(yu3000)), Neg(Succ(yu400000))) → new_primEqNat0(yu3000, yu400000)
new_esEs24(yu300, yu40000, ty_Bool) → new_esEs18(yu300, yu40000)
new_esEs21(yu301, yu40001, app(ty_Ratio, fc)) → new_esEs8(yu301, yu40001, fc)
new_esEs11(Left(yu300), Left(yu40000), ty_Integer, bcg) → new_esEs10(yu300, yu40000)
new_esEs4(yu30, yu4000, ty_Char) → new_esEs7(yu30, yu4000)
new_primPlusNat1(Succ(yu4000), Zero) → Succ(yu4000)
new_primPlusNat1(Zero, Succ(yu40001000)) → Succ(yu40001000)
new_esEs21(yu301, yu40001, ty_@0) → new_esEs16(yu301, yu40001)
new_esEs11(Left(yu300), Left(yu40000), app(app(ty_@2, bgf), bgg), bcg) → new_esEs19(yu300, yu40000, bgf, bgg)
new_esEs11(Right(yu300), Right(yu40000), bcf, ty_Float) → new_esEs15(yu300, yu40000)
new_esEs20(yu300, yu40000, ty_Int) → new_esEs12(yu300, yu40000)
new_esEs11(Left(yu300), Left(yu40000), ty_Bool, bcg) → new_esEs18(yu300, yu40000)
new_esEs9(EQ, LT) → False
new_esEs9(LT, EQ) → False
new_esEs21(yu301, yu40001, ty_Double) → new_esEs14(yu301, yu40001)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_esEs20(yu300, yu40000, ty_Char) → new_esEs7(yu300, yu40000)
new_esEs27(yu301, yu40001, ty_Int) → new_esEs12(yu301, yu40001)
new_esEs5(yu30, yu4000, ty_Integer) → new_esEs10(yu30, yu4000)
new_esEs24(yu300, yu40000, app(app(app(ty_@3, bde), bdf), bdg)) → new_esEs13(yu300, yu40000, bde, bdf, bdg)
new_esEs11(Left(yu300), Left(yu40000), app(ty_Ratio, bff), bcg) → new_esEs8(yu300, yu40000, bff)
new_esEs18(True, False) → False
new_esEs18(False, True) → False
new_primEqInt(Neg(Zero), Neg(Succ(yu400000))) → False
new_primEqInt(Neg(Succ(yu3000)), Neg(Zero)) → False
new_esEs25(yu301, yu40001, ty_Ordering) → new_esEs9(yu301, yu40001)
new_esEs8(:%(yu300, yu301), :%(yu40000, yu40001), bce) → new_asAs(new_esEs26(yu300, yu40000, bce), new_esEs27(yu301, yu40001, bce))
new_esEs19(@2(yu300, yu301), @2(yu40000, yu40001), bch, bda) → new_asAs(new_esEs24(yu300, yu40000, bch), new_esEs25(yu301, yu40001, bda))
new_esEs5(yu30, yu4000, ty_Double) → new_esEs14(yu30, yu4000)
new_esEs20(yu300, yu40000, app(app(app(ty_@3, ed), ee), ef)) → new_esEs13(yu300, yu40000, ed, ee, ef)
new_esEs24(yu300, yu40000, ty_Ordering) → new_esEs9(yu300, yu40000)
new_esEs11(Right(yu300), Right(yu40000), bcf, ty_@0) → new_esEs16(yu300, yu40000)
new_esEs25(yu301, yu40001, app(app(ty_Either, bee), bef)) → new_esEs11(yu301, yu40001, bee, bef)
new_esEs4(yu30, yu4000, app(app(ty_@2, bch), bda)) → new_esEs19(yu30, yu4000, bch, bda)
new_primPlusNat1(Zero, Zero) → Zero
new_esEs22(yu302, yu40002, ty_Int) → new_esEs12(yu302, yu40002)
new_esEs11(Left(yu300), Left(yu40000), app(ty_Maybe, bge), bcg) → new_esEs6(yu300, yu40000, bge)
new_esEs11(Left(yu300), Left(yu40000), ty_@0, bcg) → new_esEs16(yu300, yu40000)
new_asAs(True, yu39) → yu39
new_esEs11(Left(yu300), Left(yu40000), ty_Ordering, bcg) → new_esEs9(yu300, yu40000)
new_primMulNat0(Succ(yu30100), Succ(yu4000100)) → new_primPlusNat0(new_primMulNat0(yu30100, Succ(yu4000100)), yu4000100)
new_esEs6(Nothing, Nothing, cb) → True
new_primEqInt(Pos(Succ(yu3000)), Pos(Succ(yu400000))) → new_primEqNat0(yu3000, yu400000)
new_esEs26(yu300, yu40000, ty_Integer) → new_esEs10(yu300, yu40000)
new_esEs4(yu30, yu4000, ty_Ordering) → new_esEs9(yu30, yu4000)
new_esEs21(yu301, yu40001, app(ty_Maybe, gc)) → new_esEs6(yu301, yu40001, gc)
new_esEs17([], [], hh) → True
new_esEs17(:(yu300, yu301), [], hh) → False
new_esEs17([], :(yu40000, yu40001), hh) → False
new_esEs22(yu302, yu40002, app(app(ty_Either, gg), gh)) → new_esEs11(yu302, yu40002, gg, gh)
new_esEs11(Right(yu300), Right(yu40000), bcf, ty_Bool) → new_esEs18(yu300, yu40000)
new_esEs5(yu30, yu4000, app(ty_[], bca)) → new_esEs17(yu30, yu4000, bca)
new_esEs6(Just(yu300), Nothing, cb) → False
new_esEs6(Nothing, Just(yu40000), cb) → False
new_esEs23(yu300, yu40000, app(app(ty_@2, bba), bbb)) → new_esEs19(yu300, yu40000, bba, bbb)
new_primEqNat0(Succ(yu3000), Succ(yu400000)) → new_primEqNat0(yu3000, yu400000)
new_esEs24(yu300, yu40000, ty_@0) → new_esEs16(yu300, yu40000)
new_esEs24(yu300, yu40000, app(ty_Maybe, bea)) → new_esEs6(yu300, yu40000, bea)
new_esEs11(Left(yu300), Left(yu40000), app(app(app(ty_@3, bga), bgb), bgc), bcg) → new_esEs13(yu300, yu40000, bga, bgb, bgc)
new_esEs25(yu301, yu40001, app(app(ty_@2, bfd), bfe)) → new_esEs19(yu301, yu40001, bfd, bfe)
new_esEs20(yu300, yu40000, ty_Double) → new_esEs14(yu300, yu40000)
new_esEs9(LT, LT) → True
new_esEs11(Right(yu300), Right(yu40000), bcf, ty_Int) → new_esEs12(yu300, yu40000)
new_esEs20(yu300, yu40000, ty_Float) → new_esEs15(yu300, yu40000)
new_esEs21(yu301, yu40001, ty_Char) → new_esEs7(yu301, yu40001)
new_esEs5(yu30, yu4000, ty_Float) → new_esEs15(yu30, yu4000)
new_esEs11(Left(yu300), Left(yu40000), ty_Int, bcg) → new_esEs12(yu300, yu40000)
new_esEs24(yu300, yu40000, app(app(ty_Either, bdc), bdd)) → new_esEs11(yu300, yu40000, bdc, bdd)
new_esEs6(Just(yu300), Just(yu40000), ty_Char) → new_esEs7(yu300, yu40000)
new_primEqInt(Pos(Zero), Pos(Succ(yu400000))) → False
new_primEqInt(Pos(Succ(yu3000)), Pos(Zero)) → False
new_esEs24(yu300, yu40000, app(app(ty_@2, beb), bec)) → new_esEs19(yu300, yu40000, beb, bec)
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_esEs24(yu300, yu40000, ty_Float) → new_esEs15(yu300, yu40000)
new_esEs24(yu300, yu40000, ty_Double) → new_esEs14(yu300, yu40000)
new_esEs6(Just(yu300), Just(yu40000), ty_Integer) → new_esEs10(yu300, yu40000)
new_esEs18(False, False) → True
new_esEs11(Left(yu300), Right(yu40000), bcf, bcg) → False
new_esEs11(Right(yu300), Left(yu40000), bcf, bcg) → False

The set Q consists of the following terms:

new_esEs23(x0, x1, ty_Int)
new_esEs21(x0, x1, ty_Int)
new_esEs9(GT, GT)
new_esEs25(x0, x1, ty_Double)
new_esEs4(x0, x1, ty_Bool)
new_esEs27(x0, x1, ty_Int)
new_esEs4(x0, x1, ty_Integer)
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_esEs22(x0, x1, ty_Ordering)
new_esEs5(x0, x1, ty_Char)
new_primEqInt(Neg(Zero), Pos(Zero))
new_primEqInt(Pos(Zero), Neg(Zero))
new_esEs22(x0, x1, ty_Char)
new_esEs4(x0, x1, ty_Char)
new_esEs5(x0, x1, ty_Float)
new_esEs4(x0, x1, app(app(ty_Either, x2), x3))
new_esEs25(x0, x1, ty_Integer)
new_esEs20(x0, x1, ty_Bool)
new_esEs11(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs11(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs10(Integer(x0), Integer(x1))
new_esEs6(Nothing, Just(x0), x1)
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs18(False, True)
new_esEs18(True, False)
new_esEs4(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs5(x0, x1, ty_Bool)
new_esEs6(Just(x0), Just(x1), ty_Double)
new_esEs9(EQ, EQ)
new_esEs25(x0, x1, ty_Bool)
new_esEs11(Right(x0), Right(x1), x2, ty_Int)
new_esEs24(x0, x1, ty_Ordering)
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs11(Right(x0), Right(x1), x2, ty_Integer)
new_esEs6(Just(x0), Nothing, x1)
new_esEs4(x0, x1, ty_@0)
new_esEs11(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs19(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs22(x0, x1, ty_@0)
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs6(Just(x0), Just(x1), ty_@0)
new_esEs5(x0, x1, app(ty_Maybe, x2))
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs11(Left(x0), Left(x1), ty_Float, x2)
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_esEs11(Right(x0), Right(x1), x2, ty_Char)
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_sr(Neg(x0), Neg(x1))
new_esEs22(x0, x1, ty_Int)
new_esEs17([], :(x0, x1), x2)
new_esEs4(x0, x1, ty_Double)
new_esEs18(True, True)
new_esEs6(Just(x0), Just(x1), ty_Integer)
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_esEs20(x0, x1, ty_Char)
new_esEs7(Char(x0), Char(x1))
new_esEs5(x0, x1, ty_@0)
new_esEs9(LT, GT)
new_esEs9(GT, LT)
new_esEs11(Right(x0), Right(x1), x2, ty_Ordering)
new_primPlusNat0(Zero, x0)
new_esEs25(x0, x1, app(ty_[], x2))
new_esEs24(x0, x1, ty_Bool)
new_esEs16(@0, @0)
new_esEs6(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs21(x0, x1, ty_Ordering)
new_esEs6(Just(x0), Just(x1), ty_Float)
new_esEs23(x0, x1, ty_Ordering)
new_esEs9(GT, EQ)
new_esEs9(EQ, GT)
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_asAs(False, x0)
new_esEs4(x0, x1, ty_Ordering)
new_esEs5(x0, x1, ty_Double)
new_esEs23(x0, x1, ty_Char)
new_esEs20(x0, x1, ty_Integer)
new_esEs6(Just(x0), Just(x1), ty_Bool)
new_esEs17(:(x0, x1), [], x2)
new_esEs5(x0, x1, ty_Ordering)
new_primPlusNat1(Zero, Succ(x0))
new_esEs11(Left(x0), Left(x1), ty_Int, x2)
new_esEs24(x0, x1, ty_Char)
new_esEs4(x0, x1, ty_Float)
new_esEs25(x0, x1, ty_Char)
new_esEs20(x0, x1, app(ty_[], x2))
new_esEs20(x0, x1, ty_Int)
new_esEs5(x0, x1, app(ty_Ratio, x2))
new_esEs26(x0, x1, ty_Int)
new_esEs23(x0, x1, ty_Bool)
new_primEqNat0(Zero, Zero)
new_esEs23(x0, x1, ty_Integer)
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_primMulNat0(Zero, Succ(x0))
new_esEs11(Left(x0), Left(x1), ty_@0, x2)
new_primEqNat0(Succ(x0), Zero)
new_esEs20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs24(x0, x1, ty_Float)
new_esEs6(Just(x0), Just(x1), ty_Int)
new_esEs22(x0, x1, ty_Bool)
new_primPlusNat0(Succ(x0), x1)
new_esEs6(Nothing, Nothing, x0)
new_esEs6(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs11(Right(x0), Right(x1), x2, ty_@0)
new_esEs11(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_esEs21(x0, x1, ty_Float)
new_primMulNat0(Zero, Zero)
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_asAs(True, x0)
new_esEs20(x0, x1, ty_Ordering)
new_esEs5(x0, x1, ty_Integer)
new_esEs21(x0, x1, app(ty_Ratio, x2))
new_esEs21(x0, x1, ty_@0)
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs5(x0, x1, ty_Int)
new_esEs6(Just(x0), Just(x1), ty_Char)
new_esEs11(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs22(x0, x1, app(ty_[], x2))
new_esEs13(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs11(Left(x0), Left(x1), ty_Bool, x2)
new_esEs20(x0, x1, ty_Double)
new_primMulNat0(Succ(x0), Zero)
new_esEs6(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs11(Right(x0), Right(x1), x2, ty_Bool)
new_esEs11(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_sr(Pos(x0), Pos(x1))
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_esEs20(x0, x1, ty_Float)
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs22(x0, x1, ty_Double)
new_esEs11(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs12(x0, x1)
new_esEs5(x0, x1, app(ty_[], x2))
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs11(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs9(LT, EQ)
new_esEs9(EQ, LT)
new_esEs15(Float(x0, x1), Float(x2, x3))
new_esEs11(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs23(x0, x1, ty_Double)
new_esEs6(Just(x0), Just(x1), app(ty_[], x2))
new_esEs25(x0, x1, ty_Int)
new_esEs4(x0, x1, app(ty_[], x2))
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs17(:(x0, x1), :(x2, x3), x4)
new_esEs23(x0, x1, ty_Float)
new_esEs25(x0, x1, ty_Ordering)
new_esEs11(Left(x0), Left(x1), ty_Double, x2)
new_esEs24(x0, x1, app(ty_[], x2))
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs18(False, False)
new_esEs21(x0, x1, ty_Double)
new_esEs20(x0, x1, app(ty_Ratio, x2))
new_esEs4(x0, x1, app(ty_Ratio, x2))
new_esEs24(x0, x1, ty_Int)
new_esEs21(x0, x1, app(ty_[], x2))
new_esEs4(x0, x1, ty_Int)
new_esEs22(x0, x1, ty_Integer)
new_esEs20(x0, x1, ty_@0)
new_esEs23(x0, x1, ty_@0)
new_esEs11(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs20(x0, x1, app(app(ty_Either, x2), x3))
new_esEs11(Left(x0), Left(x1), ty_Integer, x2)
new_primPlusNat1(Succ(x0), Zero)
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs6(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs23(x0, x1, app(ty_[], x2))
new_primMulNat0(Succ(x0), Succ(x1))
new_primPlusNat1(Zero, Zero)
new_esEs24(x0, x1, ty_Double)
new_esEs17([], [], x0)
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs27(x0, x1, ty_Integer)
new_esEs22(x0, x1, ty_Float)
new_esEs26(x0, x1, ty_Integer)
new_esEs24(x0, x1, app(ty_Maybe, x2))
new_esEs4(x0, x1, app(ty_Maybe, x2))
new_esEs5(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs25(x0, x1, ty_@0)
new_esEs5(x0, x1, app(app(ty_Either, x2), x3))
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs11(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs11(Right(x0), Right(x1), x2, ty_Double)
new_esEs4(x0, x1, app(app(ty_@2, x2), x3))
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_esEs6(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs6(Just(x0), Just(x1), ty_Ordering)
new_esEs11(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs21(x0, x1, ty_Char)
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs11(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_esEs25(x0, x1, ty_Float)
new_esEs11(Left(x0), Right(x1), x2, x3)
new_esEs11(Right(x0), Left(x1), x2, x3)
new_esEs24(x0, x1, ty_@0)
new_esEs5(x0, x1, app(app(ty_@2, x2), x3))
new_primEqNat0(Zero, Succ(x0))
new_esEs8(:%(x0, x1), :%(x2, x3), x4)
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_esEs21(x0, x1, ty_Bool)
new_esEs24(x0, x1, ty_Integer)
new_esEs11(Right(x0), Right(x1), x2, ty_Float)
new_esEs11(Left(x0), Left(x1), ty_Char, x2)
new_esEs20(x0, x1, app(ty_Maybe, x2))
new_esEs9(LT, LT)
new_esEs14(Double(x0, x1), Double(x2, x3))
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_sr(Neg(x0), Pos(x1))
new_sr(Pos(x0), Neg(x1))
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_esEs20(x0, x1, app(app(ty_@2, x2), x3))
new_esEs21(x0, x1, ty_Integer)
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
                ↳ DependencyGraphProof
                  ↳ AND
                    ↳ QDP
                    ↳ QDP
                      ↳ UsableRulesProof
QDP
                          ↳ QReductionProof

Q DP problem:
The TRS P consists of the following rules:

new_lookup(Left(yu30), :(@2(Right(yu4000), yu401), yu41), bd, be, bf) → new_lookup(Left(yu30), yu41, bd, be, bf)
new_lookup1(yu11, yu12, yu13, yu14, False, ba, bb, bc) → new_lookup(Left(yu11), yu14, ba, bb, bc)
new_lookup(Left(yu30), :(@2(Left(yu4000), yu401), yu41), bd, be, bf) → new_lookup1(yu30, yu4000, yu401, yu41, new_esEs4(yu30, yu4000, be), bd, be, bf)

The TRS R consists of the following rules:

new_esEs4(yu30, yu4000, ty_@0) → new_esEs16(yu30, yu4000)
new_esEs4(yu30, yu4000, app(app(app(ty_@3, df), dg), dh)) → new_esEs13(yu30, yu4000, df, dg, dh)
new_esEs4(yu30, yu4000, app(app(ty_Either, bcf), bcg)) → new_esEs11(yu30, yu4000, bcf, bcg)
new_esEs4(yu30, yu4000, app(ty_[], hh)) → new_esEs17(yu30, yu4000, hh)
new_esEs4(yu30, yu4000, ty_Int) → new_esEs12(yu30, yu4000)
new_esEs4(yu30, yu4000, app(ty_Maybe, cb)) → new_esEs6(yu30, yu4000, cb)
new_esEs4(yu30, yu4000, ty_Float) → new_esEs15(yu30, yu4000)
new_esEs4(yu30, yu4000, ty_Double) → new_esEs14(yu30, yu4000)
new_esEs4(yu30, yu4000, app(ty_Ratio, bce)) → new_esEs8(yu30, yu4000, bce)
new_esEs4(yu30, yu4000, ty_Bool) → new_esEs18(yu30, yu4000)
new_esEs4(yu30, yu4000, ty_Integer) → new_esEs10(yu30, yu4000)
new_esEs4(yu30, yu4000, ty_Char) → new_esEs7(yu30, yu4000)
new_esEs4(yu30, yu4000, app(app(ty_@2, bch), bda)) → new_esEs19(yu30, yu4000, bch, bda)
new_esEs4(yu30, yu4000, ty_Ordering) → new_esEs9(yu30, yu4000)
new_esEs9(GT, LT) → False
new_esEs9(LT, GT) → False
new_esEs9(GT, GT) → True
new_esEs9(GT, EQ) → False
new_esEs9(EQ, GT) → False
new_esEs9(EQ, EQ) → True
new_esEs9(EQ, LT) → False
new_esEs9(LT, EQ) → False
new_esEs9(LT, LT) → True
new_esEs19(@2(yu300, yu301), @2(yu40000, yu40001), bch, bda) → new_asAs(new_esEs24(yu300, yu40000, bch), new_esEs25(yu301, yu40001, bda))
new_esEs24(yu300, yu40000, app(ty_[], bdh)) → new_esEs17(yu300, yu40000, bdh)
new_esEs24(yu300, yu40000, ty_Char) → new_esEs7(yu300, yu40000)
new_esEs24(yu300, yu40000, app(ty_Ratio, bdb)) → new_esEs8(yu300, yu40000, bdb)
new_esEs24(yu300, yu40000, ty_Int) → new_esEs12(yu300, yu40000)
new_esEs24(yu300, yu40000, ty_Integer) → new_esEs10(yu300, yu40000)
new_esEs24(yu300, yu40000, ty_Bool) → new_esEs18(yu300, yu40000)
new_esEs24(yu300, yu40000, app(app(app(ty_@3, bde), bdf), bdg)) → new_esEs13(yu300, yu40000, bde, bdf, bdg)
new_esEs24(yu300, yu40000, ty_Ordering) → new_esEs9(yu300, yu40000)
new_esEs24(yu300, yu40000, ty_@0) → new_esEs16(yu300, yu40000)
new_esEs24(yu300, yu40000, app(ty_Maybe, bea)) → new_esEs6(yu300, yu40000, bea)
new_esEs24(yu300, yu40000, app(app(ty_Either, bdc), bdd)) → new_esEs11(yu300, yu40000, bdc, bdd)
new_esEs24(yu300, yu40000, app(app(ty_@2, beb), bec)) → new_esEs19(yu300, yu40000, beb, bec)
new_esEs24(yu300, yu40000, ty_Float) → new_esEs15(yu300, yu40000)
new_esEs24(yu300, yu40000, ty_Double) → new_esEs14(yu300, yu40000)
new_esEs25(yu301, yu40001, ty_Float) → new_esEs15(yu301, yu40001)
new_esEs25(yu301, yu40001, ty_Integer) → new_esEs10(yu301, yu40001)
new_esEs25(yu301, yu40001, ty_Double) → new_esEs14(yu301, yu40001)
new_esEs25(yu301, yu40001, app(ty_Maybe, bfc)) → new_esEs6(yu301, yu40001, bfc)
new_esEs25(yu301, yu40001, ty_Int) → new_esEs12(yu301, yu40001)
new_esEs25(yu301, yu40001, ty_@0) → new_esEs16(yu301, yu40001)
new_esEs25(yu301, yu40001, ty_Bool) → new_esEs18(yu301, yu40001)
new_esEs25(yu301, yu40001, app(ty_Ratio, bed)) → new_esEs8(yu301, yu40001, bed)
new_esEs25(yu301, yu40001, ty_Char) → new_esEs7(yu301, yu40001)
new_esEs25(yu301, yu40001, app(ty_[], bfb)) → new_esEs17(yu301, yu40001, bfb)
new_esEs25(yu301, yu40001, app(app(app(ty_@3, beg), beh), bfa)) → new_esEs13(yu301, yu40001, beg, beh, bfa)
new_esEs25(yu301, yu40001, ty_Ordering) → new_esEs9(yu301, yu40001)
new_esEs25(yu301, yu40001, app(app(ty_Either, bee), bef)) → new_esEs11(yu301, yu40001, bee, bef)
new_esEs25(yu301, yu40001, app(app(ty_@2, bfd), bfe)) → new_esEs19(yu301, yu40001, bfd, bfe)
new_asAs(False, yu39) → False
new_asAs(True, yu39) → yu39
new_esEs11(Right(yu300), Right(yu40000), bcf, app(ty_[], bhf)) → new_esEs17(yu300, yu40000, bhf)
new_esEs11(Right(yu300), Right(yu40000), bcf, ty_Integer) → new_esEs10(yu300, yu40000)
new_esEs6(Just(yu300), Just(yu40000), app(ty_Maybe, dc)) → new_esEs6(yu300, yu40000, dc)
new_esEs11(Left(yu300), Left(yu40000), app(app(ty_Either, bfg), bfh), bcg) → new_esEs11(yu300, yu40000, bfg, bfh)
new_esEs11(Right(yu300), Right(yu40000), bcf, app(app(ty_Either, bha), bhb)) → new_esEs11(yu300, yu40000, bha, bhb)
new_esEs11(Right(yu300), Right(yu40000), bcf, app(ty_Maybe, bhg)) → new_esEs6(yu300, yu40000, bhg)
new_esEs11(Left(yu300), Left(yu40000), app(ty_Maybe, bge), bcg) → new_esEs6(yu300, yu40000, bge)
new_esEs6(Just(yu300), Just(yu40000), app(app(ty_Either, cd), ce)) → new_esEs11(yu300, yu40000, cd, ce)
new_esEs11(Left(yu300), Left(yu40000), ty_Char, bcg) → new_esEs7(yu300, yu40000)
new_esEs11(Right(yu300), Right(yu40000), bcf, ty_Char) → new_esEs7(yu300, yu40000)
new_esEs11(Right(yu300), Right(yu40000), bcf, app(ty_Ratio, bgh)) → new_esEs8(yu300, yu40000, bgh)
new_esEs11(Right(yu300), Right(yu40000), bcf, app(app(ty_@2, bhh), caa)) → new_esEs19(yu300, yu40000, bhh, caa)
new_esEs11(Right(yu300), Right(yu40000), bcf, app(app(app(ty_@3, bhc), bhd), bhe)) → new_esEs13(yu300, yu40000, bhc, bhd, bhe)
new_esEs11(Left(yu300), Left(yu40000), ty_Float, bcg) → new_esEs15(yu300, yu40000)
new_esEs11(Right(yu300), Right(yu40000), bcf, ty_Ordering) → new_esEs9(yu300, yu40000)
new_esEs11(Left(yu300), Left(yu40000), ty_Double, bcg) → new_esEs14(yu300, yu40000)
new_esEs11(Left(yu300), Left(yu40000), app(ty_[], bgd), bcg) → new_esEs17(yu300, yu40000, bgd)
new_esEs11(Right(yu300), Right(yu40000), bcf, ty_Double) → new_esEs14(yu300, yu40000)
new_esEs11(Left(yu300), Left(yu40000), ty_Integer, bcg) → new_esEs10(yu300, yu40000)
new_esEs11(Left(yu300), Left(yu40000), app(app(ty_@2, bgf), bgg), bcg) → new_esEs19(yu300, yu40000, bgf, bgg)
new_esEs11(Right(yu300), Right(yu40000), bcf, ty_Float) → new_esEs15(yu300, yu40000)
new_esEs11(Left(yu300), Left(yu40000), ty_Bool, bcg) → new_esEs18(yu300, yu40000)
new_esEs11(Left(yu300), Left(yu40000), app(ty_Ratio, bff), bcg) → new_esEs8(yu300, yu40000, bff)
new_esEs11(Right(yu300), Right(yu40000), bcf, ty_@0) → new_esEs16(yu300, yu40000)
new_esEs11(Left(yu300), Left(yu40000), ty_@0, bcg) → new_esEs16(yu300, yu40000)
new_esEs11(Left(yu300), Left(yu40000), ty_Ordering, bcg) → new_esEs9(yu300, yu40000)
new_esEs11(Right(yu300), Right(yu40000), bcf, ty_Bool) → new_esEs18(yu300, yu40000)
new_esEs11(Left(yu300), Left(yu40000), app(app(app(ty_@3, bga), bgb), bgc), bcg) → new_esEs13(yu300, yu40000, bga, bgb, bgc)
new_esEs11(Right(yu300), Right(yu40000), bcf, ty_Int) → new_esEs12(yu300, yu40000)
new_esEs11(Left(yu300), Left(yu40000), ty_Int, bcg) → new_esEs12(yu300, yu40000)
new_esEs11(Left(yu300), Right(yu40000), bcf, bcg) → False
new_esEs11(Right(yu300), Left(yu40000), bcf, bcg) → False
new_esEs12(yu30, yu4000) → new_primEqInt(yu30, yu4000)
new_primEqInt(Neg(Succ(yu3000)), Pos(yu40000)) → False
new_primEqInt(Pos(Succ(yu3000)), Neg(yu40000)) → False
new_primEqInt(Neg(Zero), Pos(Succ(yu400000))) → False
new_primEqInt(Pos(Zero), Neg(Succ(yu400000))) → False
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_primEqInt(Neg(Succ(yu3000)), Neg(Succ(yu400000))) → new_primEqNat0(yu3000, yu400000)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_primEqInt(Neg(Zero), Neg(Succ(yu400000))) → False
new_primEqInt(Neg(Succ(yu3000)), Neg(Zero)) → False
new_primEqInt(Pos(Succ(yu3000)), Pos(Succ(yu400000))) → new_primEqNat0(yu3000, yu400000)
new_primEqInt(Pos(Zero), Pos(Succ(yu400000))) → False
new_primEqInt(Pos(Succ(yu3000)), Pos(Zero)) → False
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_primEqNat0(Zero, Succ(yu400000)) → False
new_primEqNat0(Succ(yu3000), Zero) → False
new_primEqNat0(Zero, Zero) → True
new_primEqNat0(Succ(yu3000), Succ(yu400000)) → new_primEqNat0(yu3000, yu400000)
new_esEs13(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), df, dg, dh) → new_asAs(new_esEs20(yu300, yu40000, df), new_asAs(new_esEs21(yu301, yu40001, dg), new_esEs22(yu302, yu40002, dh)))
new_esEs20(yu300, yu40000, ty_@0) → new_esEs16(yu300, yu40000)
new_esEs20(yu300, yu40000, ty_Bool) → new_esEs18(yu300, yu40000)
new_esEs20(yu300, yu40000, ty_Integer) → new_esEs10(yu300, yu40000)
new_esEs20(yu300, yu40000, app(app(ty_Either, eb), ec)) → new_esEs11(yu300, yu40000, eb, ec)
new_esEs20(yu300, yu40000, app(app(ty_@2, fa), fb)) → new_esEs19(yu300, yu40000, fa, fb)
new_esEs20(yu300, yu40000, app(ty_[], eg)) → new_esEs17(yu300, yu40000, eg)
new_esEs20(yu300, yu40000, app(ty_Maybe, eh)) → new_esEs6(yu300, yu40000, eh)
new_esEs20(yu300, yu40000, app(ty_Ratio, ea)) → new_esEs8(yu300, yu40000, ea)
new_esEs20(yu300, yu40000, ty_Ordering) → new_esEs9(yu300, yu40000)
new_esEs20(yu300, yu40000, ty_Int) → new_esEs12(yu300, yu40000)
new_esEs20(yu300, yu40000, ty_Char) → new_esEs7(yu300, yu40000)
new_esEs20(yu300, yu40000, app(app(app(ty_@3, ed), ee), ef)) → new_esEs13(yu300, yu40000, ed, ee, ef)
new_esEs20(yu300, yu40000, ty_Double) → new_esEs14(yu300, yu40000)
new_esEs20(yu300, yu40000, ty_Float) → new_esEs15(yu300, yu40000)
new_esEs21(yu301, yu40001, ty_Float) → new_esEs15(yu301, yu40001)
new_esEs21(yu301, yu40001, app(app(ty_Either, fd), ff)) → new_esEs11(yu301, yu40001, fd, ff)
new_esEs21(yu301, yu40001, app(app(ty_@2, gd), ge)) → new_esEs19(yu301, yu40001, gd, ge)
new_esEs21(yu301, yu40001, app(ty_[], gb)) → new_esEs17(yu301, yu40001, gb)
new_esEs21(yu301, yu40001, ty_Int) → new_esEs12(yu301, yu40001)
new_esEs21(yu301, yu40001, ty_Integer) → new_esEs10(yu301, yu40001)
new_esEs21(yu301, yu40001, app(app(app(ty_@3, fg), fh), ga)) → new_esEs13(yu301, yu40001, fg, fh, ga)
new_esEs21(yu301, yu40001, ty_Bool) → new_esEs18(yu301, yu40001)
new_esEs21(yu301, yu40001, ty_Ordering) → new_esEs9(yu301, yu40001)
new_esEs21(yu301, yu40001, app(ty_Ratio, fc)) → new_esEs8(yu301, yu40001, fc)
new_esEs21(yu301, yu40001, ty_@0) → new_esEs16(yu301, yu40001)
new_esEs21(yu301, yu40001, ty_Double) → new_esEs14(yu301, yu40001)
new_esEs21(yu301, yu40001, app(ty_Maybe, gc)) → new_esEs6(yu301, yu40001, gc)
new_esEs21(yu301, yu40001, ty_Char) → new_esEs7(yu301, yu40001)
new_esEs22(yu302, yu40002, ty_Bool) → new_esEs18(yu302, yu40002)
new_esEs22(yu302, yu40002, ty_Ordering) → new_esEs9(yu302, yu40002)
new_esEs22(yu302, yu40002, ty_@0) → new_esEs16(yu302, yu40002)
new_esEs22(yu302, yu40002, ty_Char) → new_esEs7(yu302, yu40002)
new_esEs22(yu302, yu40002, app(ty_Ratio, gf)) → new_esEs8(yu302, yu40002, gf)
new_esEs22(yu302, yu40002, app(ty_Maybe, he)) → new_esEs6(yu302, yu40002, he)
new_esEs22(yu302, yu40002, ty_Integer) → new_esEs10(yu302, yu40002)
new_esEs22(yu302, yu40002, ty_Double) → new_esEs14(yu302, yu40002)
new_esEs22(yu302, yu40002, app(ty_[], hd)) → new_esEs17(yu302, yu40002, hd)
new_esEs22(yu302, yu40002, app(app(ty_@2, hf), hg)) → new_esEs19(yu302, yu40002, hf, hg)
new_esEs22(yu302, yu40002, ty_Float) → new_esEs15(yu302, yu40002)
new_esEs22(yu302, yu40002, app(app(app(ty_@3, ha), hb), hc)) → new_esEs13(yu302, yu40002, ha, hb, hc)
new_esEs22(yu302, yu40002, ty_Int) → new_esEs12(yu302, yu40002)
new_esEs22(yu302, yu40002, app(app(ty_Either, gg), gh)) → new_esEs11(yu302, yu40002, gg, gh)
new_esEs15(Float(yu300, yu301), Float(yu40000, yu40001)) → new_esEs12(new_sr(yu300, yu40000), new_sr(yu301, yu40001))
new_sr(Pos(yu3010), Neg(yu400010)) → Neg(new_primMulNat0(yu3010, yu400010))
new_sr(Neg(yu3010), Pos(yu400010)) → Neg(new_primMulNat0(yu3010, yu400010))
new_sr(Neg(yu3010), Neg(yu400010)) → Pos(new_primMulNat0(yu3010, yu400010))
new_sr(Pos(yu3010), Pos(yu400010)) → Pos(new_primMulNat0(yu3010, yu400010))
new_primMulNat0(Zero, Zero) → Zero
new_primMulNat0(Succ(yu30100), Zero) → Zero
new_primMulNat0(Zero, Succ(yu4000100)) → Zero
new_primMulNat0(Succ(yu30100), Succ(yu4000100)) → new_primPlusNat0(new_primMulNat0(yu30100, Succ(yu4000100)), yu4000100)
new_primPlusNat0(Zero, yu4000100) → Succ(yu4000100)
new_primPlusNat0(Succ(yu400), yu4000100) → Succ(Succ(new_primPlusNat1(yu400, yu4000100)))
new_primPlusNat1(Succ(yu4000), Succ(yu40001000)) → Succ(Succ(new_primPlusNat1(yu4000, yu40001000)))
new_primPlusNat1(Succ(yu4000), Zero) → Succ(yu4000)
new_primPlusNat1(Zero, Succ(yu40001000)) → Succ(yu40001000)
new_primPlusNat1(Zero, Zero) → Zero
new_esEs17(:(yu300, yu301), :(yu40000, yu40001), hh) → new_asAs(new_esEs23(yu300, yu40000, hh), new_esEs17(yu301, yu40001, hh))
new_esEs17([], [], hh) → True
new_esEs17(:(yu300, yu301), [], hh) → False
new_esEs17([], :(yu40000, yu40001), hh) → False
new_esEs23(yu300, yu40000, app(ty_[], bag)) → new_esEs17(yu300, yu40000, bag)
new_esEs23(yu300, yu40000, ty_Integer) → new_esEs10(yu300, yu40000)
new_esEs23(yu300, yu40000, app(ty_Ratio, baa)) → new_esEs8(yu300, yu40000, baa)
new_esEs23(yu300, yu40000, ty_Ordering) → new_esEs9(yu300, yu40000)
new_esEs23(yu300, yu40000, app(app(ty_Either, bab), bac)) → new_esEs11(yu300, yu40000, bab, bac)
new_esEs23(yu300, yu40000, ty_Char) → new_esEs7(yu300, yu40000)
new_esEs23(yu300, yu40000, ty_Double) → new_esEs14(yu300, yu40000)
new_esEs23(yu300, yu40000, ty_@0) → new_esEs16(yu300, yu40000)
new_esEs23(yu300, yu40000, app(app(app(ty_@3, bad), bae), baf)) → new_esEs13(yu300, yu40000, bad, bae, baf)
new_esEs23(yu300, yu40000, ty_Float) → new_esEs15(yu300, yu40000)
new_esEs23(yu300, yu40000, app(ty_Maybe, bah)) → new_esEs6(yu300, yu40000, bah)
new_esEs23(yu300, yu40000, ty_Bool) → new_esEs18(yu300, yu40000)
new_esEs23(yu300, yu40000, ty_Int) → new_esEs12(yu300, yu40000)
new_esEs23(yu300, yu40000, app(app(ty_@2, bba), bbb)) → new_esEs19(yu300, yu40000, bba, bbb)
new_esEs18(True, True) → True
new_esEs18(True, False) → False
new_esEs18(False, True) → False
new_esEs18(False, False) → True
new_esEs6(Just(yu300), Just(yu40000), ty_@0) → new_esEs16(yu300, yu40000)
new_esEs6(Just(yu300), Just(yu40000), ty_Ordering) → new_esEs9(yu300, yu40000)
new_esEs6(Just(yu300), Just(yu40000), ty_Float) → new_esEs15(yu300, yu40000)
new_esEs6(Just(yu300), Just(yu40000), app(app(ty_@2, dd), de)) → new_esEs19(yu300, yu40000, dd, de)
new_esEs6(Just(yu300), Just(yu40000), app(ty_Ratio, cc)) → new_esEs8(yu300, yu40000, cc)
new_esEs6(Just(yu300), Just(yu40000), ty_Int) → new_esEs12(yu300, yu40000)
new_esEs6(Just(yu300), Just(yu40000), app(ty_[], db)) → new_esEs17(yu300, yu40000, db)
new_esEs6(Just(yu300), Just(yu40000), app(app(app(ty_@3, cf), cg), da)) → new_esEs13(yu300, yu40000, cf, cg, da)
new_esEs6(Just(yu300), Just(yu40000), ty_Bool) → new_esEs18(yu300, yu40000)
new_esEs6(Just(yu300), Just(yu40000), ty_Double) → new_esEs14(yu300, yu40000)
new_esEs6(Nothing, Nothing, cb) → True
new_esEs6(Just(yu300), Nothing, cb) → False
new_esEs6(Nothing, Just(yu40000), cb) → False
new_esEs6(Just(yu300), Just(yu40000), ty_Char) → new_esEs7(yu300, yu40000)
new_esEs6(Just(yu300), Just(yu40000), ty_Integer) → new_esEs10(yu300, yu40000)
new_esEs10(Integer(yu300), Integer(yu40000)) → new_primEqInt(yu300, yu40000)
new_esEs7(Char(yu300), Char(yu40000)) → new_primEqNat0(yu300, yu40000)
new_esEs14(Double(yu300, yu301), Double(yu40000, yu40001)) → new_esEs12(new_sr(yu300, yu40000), new_sr(yu301, yu40001))
new_esEs8(:%(yu300, yu301), :%(yu40000, yu40001), bce) → new_asAs(new_esEs26(yu300, yu40000, bce), new_esEs27(yu301, yu40001, bce))
new_esEs26(yu300, yu40000, ty_Int) → new_esEs12(yu300, yu40000)
new_esEs26(yu300, yu40000, ty_Integer) → new_esEs10(yu300, yu40000)
new_esEs27(yu301, yu40001, ty_Integer) → new_esEs10(yu301, yu40001)
new_esEs27(yu301, yu40001, ty_Int) → new_esEs12(yu301, yu40001)
new_esEs16(@0, @0) → True

The set Q consists of the following terms:

new_esEs23(x0, x1, ty_Int)
new_esEs21(x0, x1, ty_Int)
new_esEs9(GT, GT)
new_esEs25(x0, x1, ty_Double)
new_esEs4(x0, x1, ty_Bool)
new_esEs27(x0, x1, ty_Int)
new_esEs4(x0, x1, ty_Integer)
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_esEs22(x0, x1, ty_Ordering)
new_esEs5(x0, x1, ty_Char)
new_primEqInt(Neg(Zero), Pos(Zero))
new_primEqInt(Pos(Zero), Neg(Zero))
new_esEs22(x0, x1, ty_Char)
new_esEs4(x0, x1, ty_Char)
new_esEs5(x0, x1, ty_Float)
new_esEs4(x0, x1, app(app(ty_Either, x2), x3))
new_esEs25(x0, x1, ty_Integer)
new_esEs20(x0, x1, ty_Bool)
new_esEs11(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs11(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs10(Integer(x0), Integer(x1))
new_esEs6(Nothing, Just(x0), x1)
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs18(False, True)
new_esEs18(True, False)
new_esEs4(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs5(x0, x1, ty_Bool)
new_esEs6(Just(x0), Just(x1), ty_Double)
new_esEs9(EQ, EQ)
new_esEs25(x0, x1, ty_Bool)
new_esEs11(Right(x0), Right(x1), x2, ty_Int)
new_esEs24(x0, x1, ty_Ordering)
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs11(Right(x0), Right(x1), x2, ty_Integer)
new_esEs6(Just(x0), Nothing, x1)
new_esEs4(x0, x1, ty_@0)
new_esEs11(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs19(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs22(x0, x1, ty_@0)
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs6(Just(x0), Just(x1), ty_@0)
new_esEs5(x0, x1, app(ty_Maybe, x2))
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs11(Left(x0), Left(x1), ty_Float, x2)
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_esEs11(Right(x0), Right(x1), x2, ty_Char)
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_sr(Neg(x0), Neg(x1))
new_esEs22(x0, x1, ty_Int)
new_esEs17([], :(x0, x1), x2)
new_esEs4(x0, x1, ty_Double)
new_esEs18(True, True)
new_esEs6(Just(x0), Just(x1), ty_Integer)
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_esEs20(x0, x1, ty_Char)
new_esEs7(Char(x0), Char(x1))
new_esEs5(x0, x1, ty_@0)
new_esEs9(LT, GT)
new_esEs9(GT, LT)
new_esEs11(Right(x0), Right(x1), x2, ty_Ordering)
new_primPlusNat0(Zero, x0)
new_esEs25(x0, x1, app(ty_[], x2))
new_esEs24(x0, x1, ty_Bool)
new_esEs16(@0, @0)
new_esEs6(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs21(x0, x1, ty_Ordering)
new_esEs6(Just(x0), Just(x1), ty_Float)
new_esEs23(x0, x1, ty_Ordering)
new_esEs9(GT, EQ)
new_esEs9(EQ, GT)
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_asAs(False, x0)
new_esEs4(x0, x1, ty_Ordering)
new_esEs5(x0, x1, ty_Double)
new_esEs23(x0, x1, ty_Char)
new_esEs20(x0, x1, ty_Integer)
new_esEs6(Just(x0), Just(x1), ty_Bool)
new_esEs17(:(x0, x1), [], x2)
new_esEs5(x0, x1, ty_Ordering)
new_primPlusNat1(Zero, Succ(x0))
new_esEs11(Left(x0), Left(x1), ty_Int, x2)
new_esEs24(x0, x1, ty_Char)
new_esEs4(x0, x1, ty_Float)
new_esEs25(x0, x1, ty_Char)
new_esEs20(x0, x1, app(ty_[], x2))
new_esEs20(x0, x1, ty_Int)
new_esEs5(x0, x1, app(ty_Ratio, x2))
new_esEs26(x0, x1, ty_Int)
new_esEs23(x0, x1, ty_Bool)
new_primEqNat0(Zero, Zero)
new_esEs23(x0, x1, ty_Integer)
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_primMulNat0(Zero, Succ(x0))
new_esEs11(Left(x0), Left(x1), ty_@0, x2)
new_primEqNat0(Succ(x0), Zero)
new_esEs20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs24(x0, x1, ty_Float)
new_esEs6(Just(x0), Just(x1), ty_Int)
new_esEs22(x0, x1, ty_Bool)
new_primPlusNat0(Succ(x0), x1)
new_esEs6(Nothing, Nothing, x0)
new_esEs6(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs11(Right(x0), Right(x1), x2, ty_@0)
new_esEs11(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_esEs21(x0, x1, ty_Float)
new_primMulNat0(Zero, Zero)
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_asAs(True, x0)
new_esEs20(x0, x1, ty_Ordering)
new_esEs5(x0, x1, ty_Integer)
new_esEs21(x0, x1, app(ty_Ratio, x2))
new_esEs21(x0, x1, ty_@0)
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs5(x0, x1, ty_Int)
new_esEs6(Just(x0), Just(x1), ty_Char)
new_esEs11(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs22(x0, x1, app(ty_[], x2))
new_esEs13(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs11(Left(x0), Left(x1), ty_Bool, x2)
new_esEs20(x0, x1, ty_Double)
new_primMulNat0(Succ(x0), Zero)
new_esEs6(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs11(Right(x0), Right(x1), x2, ty_Bool)
new_esEs11(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_sr(Pos(x0), Pos(x1))
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_esEs20(x0, x1, ty_Float)
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs22(x0, x1, ty_Double)
new_esEs11(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs12(x0, x1)
new_esEs5(x0, x1, app(ty_[], x2))
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs11(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs9(LT, EQ)
new_esEs9(EQ, LT)
new_esEs15(Float(x0, x1), Float(x2, x3))
new_esEs11(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs23(x0, x1, ty_Double)
new_esEs6(Just(x0), Just(x1), app(ty_[], x2))
new_esEs25(x0, x1, ty_Int)
new_esEs4(x0, x1, app(ty_[], x2))
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs17(:(x0, x1), :(x2, x3), x4)
new_esEs23(x0, x1, ty_Float)
new_esEs25(x0, x1, ty_Ordering)
new_esEs11(Left(x0), Left(x1), ty_Double, x2)
new_esEs24(x0, x1, app(ty_[], x2))
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs18(False, False)
new_esEs21(x0, x1, ty_Double)
new_esEs20(x0, x1, app(ty_Ratio, x2))
new_esEs4(x0, x1, app(ty_Ratio, x2))
new_esEs24(x0, x1, ty_Int)
new_esEs21(x0, x1, app(ty_[], x2))
new_esEs4(x0, x1, ty_Int)
new_esEs22(x0, x1, ty_Integer)
new_esEs20(x0, x1, ty_@0)
new_esEs23(x0, x1, ty_@0)
new_esEs11(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs20(x0, x1, app(app(ty_Either, x2), x3))
new_esEs11(Left(x0), Left(x1), ty_Integer, x2)
new_primPlusNat1(Succ(x0), Zero)
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs6(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs23(x0, x1, app(ty_[], x2))
new_primMulNat0(Succ(x0), Succ(x1))
new_primPlusNat1(Zero, Zero)
new_esEs24(x0, x1, ty_Double)
new_esEs17([], [], x0)
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs27(x0, x1, ty_Integer)
new_esEs22(x0, x1, ty_Float)
new_esEs26(x0, x1, ty_Integer)
new_esEs24(x0, x1, app(ty_Maybe, x2))
new_esEs4(x0, x1, app(ty_Maybe, x2))
new_esEs5(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs25(x0, x1, ty_@0)
new_esEs5(x0, x1, app(app(ty_Either, x2), x3))
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs11(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs11(Right(x0), Right(x1), x2, ty_Double)
new_esEs4(x0, x1, app(app(ty_@2, x2), x3))
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_esEs6(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs6(Just(x0), Just(x1), ty_Ordering)
new_esEs11(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs21(x0, x1, ty_Char)
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs11(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_esEs25(x0, x1, ty_Float)
new_esEs11(Left(x0), Right(x1), x2, x3)
new_esEs11(Right(x0), Left(x1), x2, x3)
new_esEs24(x0, x1, ty_@0)
new_esEs5(x0, x1, app(app(ty_@2, x2), x3))
new_primEqNat0(Zero, Succ(x0))
new_esEs8(:%(x0, x1), :%(x2, x3), x4)
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_esEs21(x0, x1, ty_Bool)
new_esEs24(x0, x1, ty_Integer)
new_esEs11(Right(x0), Right(x1), x2, ty_Float)
new_esEs11(Left(x0), Left(x1), ty_Char, x2)
new_esEs20(x0, x1, app(ty_Maybe, x2))
new_esEs9(LT, LT)
new_esEs14(Double(x0, x1), Double(x2, x3))
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_sr(Neg(x0), Pos(x1))
new_sr(Pos(x0), Neg(x1))
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_esEs20(x0, x1, app(app(ty_@2, x2), x3))
new_esEs21(x0, x1, ty_Integer)
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_esEs5(x0, x1, ty_Char)
new_esEs5(x0, x1, ty_Float)
new_esEs5(x0, x1, ty_Bool)
new_esEs5(x0, x1, app(ty_Maybe, x2))
new_esEs5(x0, x1, ty_@0)
new_esEs5(x0, x1, ty_Double)
new_esEs5(x0, x1, ty_Ordering)
new_esEs5(x0, x1, app(ty_Ratio, x2))
new_esEs5(x0, x1, ty_Integer)
new_esEs5(x0, x1, ty_Int)
new_esEs5(x0, x1, app(ty_[], x2))
new_esEs5(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs5(x0, x1, app(app(ty_Either, x2), x3))
new_esEs5(x0, x1, app(app(ty_@2, x2), x3))



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
                ↳ DependencyGraphProof
                  ↳ AND
                    ↳ QDP
                    ↳ QDP
                      ↳ UsableRulesProof
                        ↳ QDP
                          ↳ QReductionProof
QDP
                              ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_lookup(Left(yu30), :(@2(Right(yu4000), yu401), yu41), bd, be, bf) → new_lookup(Left(yu30), yu41, bd, be, bf)
new_lookup1(yu11, yu12, yu13, yu14, False, ba, bb, bc) → new_lookup(Left(yu11), yu14, ba, bb, bc)
new_lookup(Left(yu30), :(@2(Left(yu4000), yu401), yu41), bd, be, bf) → new_lookup1(yu30, yu4000, yu401, yu41, new_esEs4(yu30, yu4000, be), bd, be, bf)

The TRS R consists of the following rules:

new_esEs4(yu30, yu4000, ty_@0) → new_esEs16(yu30, yu4000)
new_esEs4(yu30, yu4000, app(app(app(ty_@3, df), dg), dh)) → new_esEs13(yu30, yu4000, df, dg, dh)
new_esEs4(yu30, yu4000, app(app(ty_Either, bcf), bcg)) → new_esEs11(yu30, yu4000, bcf, bcg)
new_esEs4(yu30, yu4000, app(ty_[], hh)) → new_esEs17(yu30, yu4000, hh)
new_esEs4(yu30, yu4000, ty_Int) → new_esEs12(yu30, yu4000)
new_esEs4(yu30, yu4000, app(ty_Maybe, cb)) → new_esEs6(yu30, yu4000, cb)
new_esEs4(yu30, yu4000, ty_Float) → new_esEs15(yu30, yu4000)
new_esEs4(yu30, yu4000, ty_Double) → new_esEs14(yu30, yu4000)
new_esEs4(yu30, yu4000, app(ty_Ratio, bce)) → new_esEs8(yu30, yu4000, bce)
new_esEs4(yu30, yu4000, ty_Bool) → new_esEs18(yu30, yu4000)
new_esEs4(yu30, yu4000, ty_Integer) → new_esEs10(yu30, yu4000)
new_esEs4(yu30, yu4000, ty_Char) → new_esEs7(yu30, yu4000)
new_esEs4(yu30, yu4000, app(app(ty_@2, bch), bda)) → new_esEs19(yu30, yu4000, bch, bda)
new_esEs4(yu30, yu4000, ty_Ordering) → new_esEs9(yu30, yu4000)
new_esEs9(GT, LT) → False
new_esEs9(LT, GT) → False
new_esEs9(GT, GT) → True
new_esEs9(GT, EQ) → False
new_esEs9(EQ, GT) → False
new_esEs9(EQ, EQ) → True
new_esEs9(EQ, LT) → False
new_esEs9(LT, EQ) → False
new_esEs9(LT, LT) → True
new_esEs19(@2(yu300, yu301), @2(yu40000, yu40001), bch, bda) → new_asAs(new_esEs24(yu300, yu40000, bch), new_esEs25(yu301, yu40001, bda))
new_esEs24(yu300, yu40000, app(ty_[], bdh)) → new_esEs17(yu300, yu40000, bdh)
new_esEs24(yu300, yu40000, ty_Char) → new_esEs7(yu300, yu40000)
new_esEs24(yu300, yu40000, app(ty_Ratio, bdb)) → new_esEs8(yu300, yu40000, bdb)
new_esEs24(yu300, yu40000, ty_Int) → new_esEs12(yu300, yu40000)
new_esEs24(yu300, yu40000, ty_Integer) → new_esEs10(yu300, yu40000)
new_esEs24(yu300, yu40000, ty_Bool) → new_esEs18(yu300, yu40000)
new_esEs24(yu300, yu40000, app(app(app(ty_@3, bde), bdf), bdg)) → new_esEs13(yu300, yu40000, bde, bdf, bdg)
new_esEs24(yu300, yu40000, ty_Ordering) → new_esEs9(yu300, yu40000)
new_esEs24(yu300, yu40000, ty_@0) → new_esEs16(yu300, yu40000)
new_esEs24(yu300, yu40000, app(ty_Maybe, bea)) → new_esEs6(yu300, yu40000, bea)
new_esEs24(yu300, yu40000, app(app(ty_Either, bdc), bdd)) → new_esEs11(yu300, yu40000, bdc, bdd)
new_esEs24(yu300, yu40000, app(app(ty_@2, beb), bec)) → new_esEs19(yu300, yu40000, beb, bec)
new_esEs24(yu300, yu40000, ty_Float) → new_esEs15(yu300, yu40000)
new_esEs24(yu300, yu40000, ty_Double) → new_esEs14(yu300, yu40000)
new_esEs25(yu301, yu40001, ty_Float) → new_esEs15(yu301, yu40001)
new_esEs25(yu301, yu40001, ty_Integer) → new_esEs10(yu301, yu40001)
new_esEs25(yu301, yu40001, ty_Double) → new_esEs14(yu301, yu40001)
new_esEs25(yu301, yu40001, app(ty_Maybe, bfc)) → new_esEs6(yu301, yu40001, bfc)
new_esEs25(yu301, yu40001, ty_Int) → new_esEs12(yu301, yu40001)
new_esEs25(yu301, yu40001, ty_@0) → new_esEs16(yu301, yu40001)
new_esEs25(yu301, yu40001, ty_Bool) → new_esEs18(yu301, yu40001)
new_esEs25(yu301, yu40001, app(ty_Ratio, bed)) → new_esEs8(yu301, yu40001, bed)
new_esEs25(yu301, yu40001, ty_Char) → new_esEs7(yu301, yu40001)
new_esEs25(yu301, yu40001, app(ty_[], bfb)) → new_esEs17(yu301, yu40001, bfb)
new_esEs25(yu301, yu40001, app(app(app(ty_@3, beg), beh), bfa)) → new_esEs13(yu301, yu40001, beg, beh, bfa)
new_esEs25(yu301, yu40001, ty_Ordering) → new_esEs9(yu301, yu40001)
new_esEs25(yu301, yu40001, app(app(ty_Either, bee), bef)) → new_esEs11(yu301, yu40001, bee, bef)
new_esEs25(yu301, yu40001, app(app(ty_@2, bfd), bfe)) → new_esEs19(yu301, yu40001, bfd, bfe)
new_asAs(False, yu39) → False
new_asAs(True, yu39) → yu39
new_esEs11(Right(yu300), Right(yu40000), bcf, app(ty_[], bhf)) → new_esEs17(yu300, yu40000, bhf)
new_esEs11(Right(yu300), Right(yu40000), bcf, ty_Integer) → new_esEs10(yu300, yu40000)
new_esEs6(Just(yu300), Just(yu40000), app(ty_Maybe, dc)) → new_esEs6(yu300, yu40000, dc)
new_esEs11(Left(yu300), Left(yu40000), app(app(ty_Either, bfg), bfh), bcg) → new_esEs11(yu300, yu40000, bfg, bfh)
new_esEs11(Right(yu300), Right(yu40000), bcf, app(app(ty_Either, bha), bhb)) → new_esEs11(yu300, yu40000, bha, bhb)
new_esEs11(Right(yu300), Right(yu40000), bcf, app(ty_Maybe, bhg)) → new_esEs6(yu300, yu40000, bhg)
new_esEs11(Left(yu300), Left(yu40000), app(ty_Maybe, bge), bcg) → new_esEs6(yu300, yu40000, bge)
new_esEs6(Just(yu300), Just(yu40000), app(app(ty_Either, cd), ce)) → new_esEs11(yu300, yu40000, cd, ce)
new_esEs11(Left(yu300), Left(yu40000), ty_Char, bcg) → new_esEs7(yu300, yu40000)
new_esEs11(Right(yu300), Right(yu40000), bcf, ty_Char) → new_esEs7(yu300, yu40000)
new_esEs11(Right(yu300), Right(yu40000), bcf, app(ty_Ratio, bgh)) → new_esEs8(yu300, yu40000, bgh)
new_esEs11(Right(yu300), Right(yu40000), bcf, app(app(ty_@2, bhh), caa)) → new_esEs19(yu300, yu40000, bhh, caa)
new_esEs11(Right(yu300), Right(yu40000), bcf, app(app(app(ty_@3, bhc), bhd), bhe)) → new_esEs13(yu300, yu40000, bhc, bhd, bhe)
new_esEs11(Left(yu300), Left(yu40000), ty_Float, bcg) → new_esEs15(yu300, yu40000)
new_esEs11(Right(yu300), Right(yu40000), bcf, ty_Ordering) → new_esEs9(yu300, yu40000)
new_esEs11(Left(yu300), Left(yu40000), ty_Double, bcg) → new_esEs14(yu300, yu40000)
new_esEs11(Left(yu300), Left(yu40000), app(ty_[], bgd), bcg) → new_esEs17(yu300, yu40000, bgd)
new_esEs11(Right(yu300), Right(yu40000), bcf, ty_Double) → new_esEs14(yu300, yu40000)
new_esEs11(Left(yu300), Left(yu40000), ty_Integer, bcg) → new_esEs10(yu300, yu40000)
new_esEs11(Left(yu300), Left(yu40000), app(app(ty_@2, bgf), bgg), bcg) → new_esEs19(yu300, yu40000, bgf, bgg)
new_esEs11(Right(yu300), Right(yu40000), bcf, ty_Float) → new_esEs15(yu300, yu40000)
new_esEs11(Left(yu300), Left(yu40000), ty_Bool, bcg) → new_esEs18(yu300, yu40000)
new_esEs11(Left(yu300), Left(yu40000), app(ty_Ratio, bff), bcg) → new_esEs8(yu300, yu40000, bff)
new_esEs11(Right(yu300), Right(yu40000), bcf, ty_@0) → new_esEs16(yu300, yu40000)
new_esEs11(Left(yu300), Left(yu40000), ty_@0, bcg) → new_esEs16(yu300, yu40000)
new_esEs11(Left(yu300), Left(yu40000), ty_Ordering, bcg) → new_esEs9(yu300, yu40000)
new_esEs11(Right(yu300), Right(yu40000), bcf, ty_Bool) → new_esEs18(yu300, yu40000)
new_esEs11(Left(yu300), Left(yu40000), app(app(app(ty_@3, bga), bgb), bgc), bcg) → new_esEs13(yu300, yu40000, bga, bgb, bgc)
new_esEs11(Right(yu300), Right(yu40000), bcf, ty_Int) → new_esEs12(yu300, yu40000)
new_esEs11(Left(yu300), Left(yu40000), ty_Int, bcg) → new_esEs12(yu300, yu40000)
new_esEs11(Left(yu300), Right(yu40000), bcf, bcg) → False
new_esEs11(Right(yu300), Left(yu40000), bcf, bcg) → False
new_esEs12(yu30, yu4000) → new_primEqInt(yu30, yu4000)
new_primEqInt(Neg(Succ(yu3000)), Pos(yu40000)) → False
new_primEqInt(Pos(Succ(yu3000)), Neg(yu40000)) → False
new_primEqInt(Neg(Zero), Pos(Succ(yu400000))) → False
new_primEqInt(Pos(Zero), Neg(Succ(yu400000))) → False
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_primEqInt(Neg(Succ(yu3000)), Neg(Succ(yu400000))) → new_primEqNat0(yu3000, yu400000)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_primEqInt(Neg(Zero), Neg(Succ(yu400000))) → False
new_primEqInt(Neg(Succ(yu3000)), Neg(Zero)) → False
new_primEqInt(Pos(Succ(yu3000)), Pos(Succ(yu400000))) → new_primEqNat0(yu3000, yu400000)
new_primEqInt(Pos(Zero), Pos(Succ(yu400000))) → False
new_primEqInt(Pos(Succ(yu3000)), Pos(Zero)) → False
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_primEqNat0(Zero, Succ(yu400000)) → False
new_primEqNat0(Succ(yu3000), Zero) → False
new_primEqNat0(Zero, Zero) → True
new_primEqNat0(Succ(yu3000), Succ(yu400000)) → new_primEqNat0(yu3000, yu400000)
new_esEs13(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), df, dg, dh) → new_asAs(new_esEs20(yu300, yu40000, df), new_asAs(new_esEs21(yu301, yu40001, dg), new_esEs22(yu302, yu40002, dh)))
new_esEs20(yu300, yu40000, ty_@0) → new_esEs16(yu300, yu40000)
new_esEs20(yu300, yu40000, ty_Bool) → new_esEs18(yu300, yu40000)
new_esEs20(yu300, yu40000, ty_Integer) → new_esEs10(yu300, yu40000)
new_esEs20(yu300, yu40000, app(app(ty_Either, eb), ec)) → new_esEs11(yu300, yu40000, eb, ec)
new_esEs20(yu300, yu40000, app(app(ty_@2, fa), fb)) → new_esEs19(yu300, yu40000, fa, fb)
new_esEs20(yu300, yu40000, app(ty_[], eg)) → new_esEs17(yu300, yu40000, eg)
new_esEs20(yu300, yu40000, app(ty_Maybe, eh)) → new_esEs6(yu300, yu40000, eh)
new_esEs20(yu300, yu40000, app(ty_Ratio, ea)) → new_esEs8(yu300, yu40000, ea)
new_esEs20(yu300, yu40000, ty_Ordering) → new_esEs9(yu300, yu40000)
new_esEs20(yu300, yu40000, ty_Int) → new_esEs12(yu300, yu40000)
new_esEs20(yu300, yu40000, ty_Char) → new_esEs7(yu300, yu40000)
new_esEs20(yu300, yu40000, app(app(app(ty_@3, ed), ee), ef)) → new_esEs13(yu300, yu40000, ed, ee, ef)
new_esEs20(yu300, yu40000, ty_Double) → new_esEs14(yu300, yu40000)
new_esEs20(yu300, yu40000, ty_Float) → new_esEs15(yu300, yu40000)
new_esEs21(yu301, yu40001, ty_Float) → new_esEs15(yu301, yu40001)
new_esEs21(yu301, yu40001, app(app(ty_Either, fd), ff)) → new_esEs11(yu301, yu40001, fd, ff)
new_esEs21(yu301, yu40001, app(app(ty_@2, gd), ge)) → new_esEs19(yu301, yu40001, gd, ge)
new_esEs21(yu301, yu40001, app(ty_[], gb)) → new_esEs17(yu301, yu40001, gb)
new_esEs21(yu301, yu40001, ty_Int) → new_esEs12(yu301, yu40001)
new_esEs21(yu301, yu40001, ty_Integer) → new_esEs10(yu301, yu40001)
new_esEs21(yu301, yu40001, app(app(app(ty_@3, fg), fh), ga)) → new_esEs13(yu301, yu40001, fg, fh, ga)
new_esEs21(yu301, yu40001, ty_Bool) → new_esEs18(yu301, yu40001)
new_esEs21(yu301, yu40001, ty_Ordering) → new_esEs9(yu301, yu40001)
new_esEs21(yu301, yu40001, app(ty_Ratio, fc)) → new_esEs8(yu301, yu40001, fc)
new_esEs21(yu301, yu40001, ty_@0) → new_esEs16(yu301, yu40001)
new_esEs21(yu301, yu40001, ty_Double) → new_esEs14(yu301, yu40001)
new_esEs21(yu301, yu40001, app(ty_Maybe, gc)) → new_esEs6(yu301, yu40001, gc)
new_esEs21(yu301, yu40001, ty_Char) → new_esEs7(yu301, yu40001)
new_esEs22(yu302, yu40002, ty_Bool) → new_esEs18(yu302, yu40002)
new_esEs22(yu302, yu40002, ty_Ordering) → new_esEs9(yu302, yu40002)
new_esEs22(yu302, yu40002, ty_@0) → new_esEs16(yu302, yu40002)
new_esEs22(yu302, yu40002, ty_Char) → new_esEs7(yu302, yu40002)
new_esEs22(yu302, yu40002, app(ty_Ratio, gf)) → new_esEs8(yu302, yu40002, gf)
new_esEs22(yu302, yu40002, app(ty_Maybe, he)) → new_esEs6(yu302, yu40002, he)
new_esEs22(yu302, yu40002, ty_Integer) → new_esEs10(yu302, yu40002)
new_esEs22(yu302, yu40002, ty_Double) → new_esEs14(yu302, yu40002)
new_esEs22(yu302, yu40002, app(ty_[], hd)) → new_esEs17(yu302, yu40002, hd)
new_esEs22(yu302, yu40002, app(app(ty_@2, hf), hg)) → new_esEs19(yu302, yu40002, hf, hg)
new_esEs22(yu302, yu40002, ty_Float) → new_esEs15(yu302, yu40002)
new_esEs22(yu302, yu40002, app(app(app(ty_@3, ha), hb), hc)) → new_esEs13(yu302, yu40002, ha, hb, hc)
new_esEs22(yu302, yu40002, ty_Int) → new_esEs12(yu302, yu40002)
new_esEs22(yu302, yu40002, app(app(ty_Either, gg), gh)) → new_esEs11(yu302, yu40002, gg, gh)
new_esEs15(Float(yu300, yu301), Float(yu40000, yu40001)) → new_esEs12(new_sr(yu300, yu40000), new_sr(yu301, yu40001))
new_sr(Pos(yu3010), Neg(yu400010)) → Neg(new_primMulNat0(yu3010, yu400010))
new_sr(Neg(yu3010), Pos(yu400010)) → Neg(new_primMulNat0(yu3010, yu400010))
new_sr(Neg(yu3010), Neg(yu400010)) → Pos(new_primMulNat0(yu3010, yu400010))
new_sr(Pos(yu3010), Pos(yu400010)) → Pos(new_primMulNat0(yu3010, yu400010))
new_primMulNat0(Zero, Zero) → Zero
new_primMulNat0(Succ(yu30100), Zero) → Zero
new_primMulNat0(Zero, Succ(yu4000100)) → Zero
new_primMulNat0(Succ(yu30100), Succ(yu4000100)) → new_primPlusNat0(new_primMulNat0(yu30100, Succ(yu4000100)), yu4000100)
new_primPlusNat0(Zero, yu4000100) → Succ(yu4000100)
new_primPlusNat0(Succ(yu400), yu4000100) → Succ(Succ(new_primPlusNat1(yu400, yu4000100)))
new_primPlusNat1(Succ(yu4000), Succ(yu40001000)) → Succ(Succ(new_primPlusNat1(yu4000, yu40001000)))
new_primPlusNat1(Succ(yu4000), Zero) → Succ(yu4000)
new_primPlusNat1(Zero, Succ(yu40001000)) → Succ(yu40001000)
new_primPlusNat1(Zero, Zero) → Zero
new_esEs17(:(yu300, yu301), :(yu40000, yu40001), hh) → new_asAs(new_esEs23(yu300, yu40000, hh), new_esEs17(yu301, yu40001, hh))
new_esEs17([], [], hh) → True
new_esEs17(:(yu300, yu301), [], hh) → False
new_esEs17([], :(yu40000, yu40001), hh) → False
new_esEs23(yu300, yu40000, app(ty_[], bag)) → new_esEs17(yu300, yu40000, bag)
new_esEs23(yu300, yu40000, ty_Integer) → new_esEs10(yu300, yu40000)
new_esEs23(yu300, yu40000, app(ty_Ratio, baa)) → new_esEs8(yu300, yu40000, baa)
new_esEs23(yu300, yu40000, ty_Ordering) → new_esEs9(yu300, yu40000)
new_esEs23(yu300, yu40000, app(app(ty_Either, bab), bac)) → new_esEs11(yu300, yu40000, bab, bac)
new_esEs23(yu300, yu40000, ty_Char) → new_esEs7(yu300, yu40000)
new_esEs23(yu300, yu40000, ty_Double) → new_esEs14(yu300, yu40000)
new_esEs23(yu300, yu40000, ty_@0) → new_esEs16(yu300, yu40000)
new_esEs23(yu300, yu40000, app(app(app(ty_@3, bad), bae), baf)) → new_esEs13(yu300, yu40000, bad, bae, baf)
new_esEs23(yu300, yu40000, ty_Float) → new_esEs15(yu300, yu40000)
new_esEs23(yu300, yu40000, app(ty_Maybe, bah)) → new_esEs6(yu300, yu40000, bah)
new_esEs23(yu300, yu40000, ty_Bool) → new_esEs18(yu300, yu40000)
new_esEs23(yu300, yu40000, ty_Int) → new_esEs12(yu300, yu40000)
new_esEs23(yu300, yu40000, app(app(ty_@2, bba), bbb)) → new_esEs19(yu300, yu40000, bba, bbb)
new_esEs18(True, True) → True
new_esEs18(True, False) → False
new_esEs18(False, True) → False
new_esEs18(False, False) → True
new_esEs6(Just(yu300), Just(yu40000), ty_@0) → new_esEs16(yu300, yu40000)
new_esEs6(Just(yu300), Just(yu40000), ty_Ordering) → new_esEs9(yu300, yu40000)
new_esEs6(Just(yu300), Just(yu40000), ty_Float) → new_esEs15(yu300, yu40000)
new_esEs6(Just(yu300), Just(yu40000), app(app(ty_@2, dd), de)) → new_esEs19(yu300, yu40000, dd, de)
new_esEs6(Just(yu300), Just(yu40000), app(ty_Ratio, cc)) → new_esEs8(yu300, yu40000, cc)
new_esEs6(Just(yu300), Just(yu40000), ty_Int) → new_esEs12(yu300, yu40000)
new_esEs6(Just(yu300), Just(yu40000), app(ty_[], db)) → new_esEs17(yu300, yu40000, db)
new_esEs6(Just(yu300), Just(yu40000), app(app(app(ty_@3, cf), cg), da)) → new_esEs13(yu300, yu40000, cf, cg, da)
new_esEs6(Just(yu300), Just(yu40000), ty_Bool) → new_esEs18(yu300, yu40000)
new_esEs6(Just(yu300), Just(yu40000), ty_Double) → new_esEs14(yu300, yu40000)
new_esEs6(Nothing, Nothing, cb) → True
new_esEs6(Just(yu300), Nothing, cb) → False
new_esEs6(Nothing, Just(yu40000), cb) → False
new_esEs6(Just(yu300), Just(yu40000), ty_Char) → new_esEs7(yu300, yu40000)
new_esEs6(Just(yu300), Just(yu40000), ty_Integer) → new_esEs10(yu300, yu40000)
new_esEs10(Integer(yu300), Integer(yu40000)) → new_primEqInt(yu300, yu40000)
new_esEs7(Char(yu300), Char(yu40000)) → new_primEqNat0(yu300, yu40000)
new_esEs14(Double(yu300, yu301), Double(yu40000, yu40001)) → new_esEs12(new_sr(yu300, yu40000), new_sr(yu301, yu40001))
new_esEs8(:%(yu300, yu301), :%(yu40000, yu40001), bce) → new_asAs(new_esEs26(yu300, yu40000, bce), new_esEs27(yu301, yu40001, bce))
new_esEs26(yu300, yu40000, ty_Int) → new_esEs12(yu300, yu40000)
new_esEs26(yu300, yu40000, ty_Integer) → new_esEs10(yu300, yu40000)
new_esEs27(yu301, yu40001, ty_Integer) → new_esEs10(yu301, yu40001)
new_esEs27(yu301, yu40001, ty_Int) → new_esEs12(yu301, yu40001)
new_esEs16(@0, @0) → True

The set Q consists of the following terms:

new_esEs23(x0, x1, ty_Int)
new_esEs21(x0, x1, ty_Int)
new_esEs9(GT, GT)
new_esEs25(x0, x1, ty_Double)
new_esEs4(x0, x1, ty_Bool)
new_esEs27(x0, x1, ty_Int)
new_esEs4(x0, x1, ty_Integer)
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_esEs22(x0, x1, ty_Ordering)
new_primEqInt(Neg(Zero), Pos(Zero))
new_primEqInt(Pos(Zero), Neg(Zero))
new_esEs22(x0, x1, ty_Char)
new_esEs4(x0, x1, ty_Char)
new_esEs4(x0, x1, app(app(ty_Either, x2), x3))
new_esEs25(x0, x1, ty_Integer)
new_esEs20(x0, x1, ty_Bool)
new_esEs11(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs11(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs10(Integer(x0), Integer(x1))
new_esEs6(Nothing, Just(x0), x1)
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs18(False, True)
new_esEs18(True, False)
new_esEs4(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs6(Just(x0), Just(x1), ty_Double)
new_esEs9(EQ, EQ)
new_esEs25(x0, x1, ty_Bool)
new_esEs11(Right(x0), Right(x1), x2, ty_Int)
new_esEs24(x0, x1, ty_Ordering)
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs11(Right(x0), Right(x1), x2, ty_Integer)
new_esEs6(Just(x0), Nothing, x1)
new_esEs4(x0, x1, ty_@0)
new_esEs11(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs19(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs22(x0, x1, ty_@0)
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs6(Just(x0), Just(x1), ty_@0)
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs11(Left(x0), Left(x1), ty_Float, x2)
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_esEs11(Right(x0), Right(x1), x2, ty_Char)
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_sr(Neg(x0), Neg(x1))
new_esEs22(x0, x1, ty_Int)
new_esEs17([], :(x0, x1), x2)
new_esEs4(x0, x1, ty_Double)
new_esEs18(True, True)
new_esEs6(Just(x0), Just(x1), ty_Integer)
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_esEs20(x0, x1, ty_Char)
new_esEs7(Char(x0), Char(x1))
new_esEs9(LT, GT)
new_esEs9(GT, LT)
new_esEs11(Right(x0), Right(x1), x2, ty_Ordering)
new_primPlusNat0(Zero, x0)
new_esEs25(x0, x1, app(ty_[], x2))
new_esEs24(x0, x1, ty_Bool)
new_esEs16(@0, @0)
new_esEs6(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs21(x0, x1, ty_Ordering)
new_esEs6(Just(x0), Just(x1), ty_Float)
new_esEs23(x0, x1, ty_Ordering)
new_esEs9(GT, EQ)
new_esEs9(EQ, GT)
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_asAs(False, x0)
new_esEs4(x0, x1, ty_Ordering)
new_esEs23(x0, x1, ty_Char)
new_esEs20(x0, x1, ty_Integer)
new_esEs6(Just(x0), Just(x1), ty_Bool)
new_esEs17(:(x0, x1), [], x2)
new_primPlusNat1(Zero, Succ(x0))
new_esEs11(Left(x0), Left(x1), ty_Int, x2)
new_esEs24(x0, x1, ty_Char)
new_esEs4(x0, x1, ty_Float)
new_esEs25(x0, x1, ty_Char)
new_esEs20(x0, x1, app(ty_[], x2))
new_esEs20(x0, x1, ty_Int)
new_esEs26(x0, x1, ty_Int)
new_esEs23(x0, x1, ty_Bool)
new_primEqNat0(Zero, Zero)
new_esEs23(x0, x1, ty_Integer)
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_primMulNat0(Zero, Succ(x0))
new_esEs11(Left(x0), Left(x1), ty_@0, x2)
new_primEqNat0(Succ(x0), Zero)
new_esEs20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs24(x0, x1, ty_Float)
new_esEs6(Just(x0), Just(x1), ty_Int)
new_esEs22(x0, x1, ty_Bool)
new_primPlusNat0(Succ(x0), x1)
new_esEs6(Nothing, Nothing, x0)
new_esEs6(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs11(Right(x0), Right(x1), x2, ty_@0)
new_esEs11(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_esEs21(x0, x1, ty_Float)
new_primMulNat0(Zero, Zero)
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_asAs(True, x0)
new_esEs20(x0, x1, ty_Ordering)
new_esEs21(x0, x1, app(ty_Ratio, x2))
new_esEs21(x0, x1, ty_@0)
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs6(Just(x0), Just(x1), ty_Char)
new_esEs11(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs22(x0, x1, app(ty_[], x2))
new_esEs13(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs11(Left(x0), Left(x1), ty_Bool, x2)
new_esEs20(x0, x1, ty_Double)
new_primMulNat0(Succ(x0), Zero)
new_esEs6(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs11(Right(x0), Right(x1), x2, ty_Bool)
new_esEs11(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_sr(Pos(x0), Pos(x1))
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_esEs20(x0, x1, ty_Float)
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs22(x0, x1, ty_Double)
new_esEs11(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs12(x0, x1)
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs11(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs9(LT, EQ)
new_esEs9(EQ, LT)
new_esEs15(Float(x0, x1), Float(x2, x3))
new_esEs11(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs23(x0, x1, ty_Double)
new_esEs6(Just(x0), Just(x1), app(ty_[], x2))
new_esEs25(x0, x1, ty_Int)
new_esEs4(x0, x1, app(ty_[], x2))
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs17(:(x0, x1), :(x2, x3), x4)
new_esEs23(x0, x1, ty_Float)
new_esEs25(x0, x1, ty_Ordering)
new_esEs11(Left(x0), Left(x1), ty_Double, x2)
new_esEs24(x0, x1, app(ty_[], x2))
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs18(False, False)
new_esEs21(x0, x1, ty_Double)
new_esEs20(x0, x1, app(ty_Ratio, x2))
new_esEs4(x0, x1, app(ty_Ratio, x2))
new_esEs24(x0, x1, ty_Int)
new_esEs21(x0, x1, app(ty_[], x2))
new_esEs4(x0, x1, ty_Int)
new_esEs22(x0, x1, ty_Integer)
new_esEs20(x0, x1, ty_@0)
new_esEs23(x0, x1, ty_@0)
new_esEs11(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs20(x0, x1, app(app(ty_Either, x2), x3))
new_esEs11(Left(x0), Left(x1), ty_Integer, x2)
new_primPlusNat1(Succ(x0), Zero)
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs6(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs23(x0, x1, app(ty_[], x2))
new_primMulNat0(Succ(x0), Succ(x1))
new_primPlusNat1(Zero, Zero)
new_esEs24(x0, x1, ty_Double)
new_esEs17([], [], x0)
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs27(x0, x1, ty_Integer)
new_esEs22(x0, x1, ty_Float)
new_esEs26(x0, x1, ty_Integer)
new_esEs24(x0, x1, app(ty_Maybe, x2))
new_esEs4(x0, x1, app(ty_Maybe, x2))
new_esEs25(x0, x1, ty_@0)
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs11(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs11(Right(x0), Right(x1), x2, ty_Double)
new_esEs4(x0, x1, app(app(ty_@2, x2), x3))
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_esEs6(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs6(Just(x0), Just(x1), ty_Ordering)
new_esEs11(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs21(x0, x1, ty_Char)
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs11(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_esEs25(x0, x1, ty_Float)
new_esEs11(Left(x0), Right(x1), x2, x3)
new_esEs11(Right(x0), Left(x1), x2, x3)
new_esEs24(x0, x1, ty_@0)
new_primEqNat0(Zero, Succ(x0))
new_esEs8(:%(x0, x1), :%(x2, x3), x4)
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_esEs21(x0, x1, ty_Bool)
new_esEs24(x0, x1, ty_Integer)
new_esEs11(Right(x0), Right(x1), x2, ty_Float)
new_esEs11(Left(x0), Left(x1), ty_Char, x2)
new_esEs20(x0, x1, app(ty_Maybe, x2))
new_esEs9(LT, LT)
new_esEs14(Double(x0, x1), Double(x2, x3))
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_sr(Neg(x0), Pos(x1))
new_sr(Pos(x0), Neg(x1))
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_esEs20(x0, x1, app(app(ty_@2, x2), x3))
new_esEs21(x0, x1, ty_Integer)
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: